1  /-
  2  Copyright (c) 2017 Mario Carneiro. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Mario Carneiro
  5  -/
  6  import tactic.basic
src         └──────────┘
  7  import data.list.basic data.stream data.lazy_list data.seq.computation logic.basic
src         └─────────────┘ └─────────┘ └────────────┘ └──────────────────┘ └─────────┘
  8  
  9  universes u v w
 10  
 11  /-
 12  coinductive seq (α : Type u) : Type u
 13  | nil : seq α
 14  | cons : α → seq α → seq α
 15  -/
 16  
 17  /--
 18  A stream `s : option α` is a sequence if `s.nth n = none` implies `s.nth (n + 1) = none`.
 19  -/
 20  def stream.is_seq {α : Type u} (s : stream (option α)) : Prop :=
id                                       └────┘  └────┘ 
src                                      └────┘  └────┘
typ                                      └────┘  └────┘ 
 21  ∀ {n : ℕ}, s n = none → s (n + 1) = none
id                └──┘           └──┘
src                 └──┘             └──┘
typ               └──┘           └──┘
 22  
 23  /-- `seq α` is the type of possibly infinite lists (referred here as sequences).
 24    It is encoded as an infinite stream of options such that if `f n = none`, then
 25    `f m = none` for all `m ≥ n`. -/
 26  def seq (α : Type u) : Type u := { f : stream (option α) // f.is_seq }
id                                         └────┘  └────┘      └─────┘
src                                        └────┘  └────┘        └─────┘
typ                                        └────┘  └────┘      └─────┘
doc                                                               └─────┘
 27  
 28  /-- `seq1 α` is the type of nonempty sequences. -/
 29  def seq1 (α) := α × seq α
id                     └─┘ 
src                     └─┘
typ                    └─┘ 
doc                      └─┘
 30  
 31  namespace seq
 32  variables {α : Type u} {β : Type v} {γ : Type w}
 33  
 34  /-- The empty sequence -/
 35  def nil : seq α := ⟨stream.const none, λn h, rfl⟩
id             └─┘      └──────────┘ └──┘      └─┘
src            └─┘       └──────────┘ └──┘        └─┘
typ            └─┘      └──────────┘ └──┘      └─┘
doc            └─┘
 36  
 37  instance : inhabited (seq α) := ⟨nil⟩
id              └───────┘  └─┘       └─┘
src             └───────┘  └─┘        └─┘
typ             └───────┘  └─┘       └─┘
doc                        └─┘        └─┘
 38  
 39  /-- Prepend an element to a sequence -/
 40  def cons (a : α) : seq α → seq α
id                     └─┘   └─┘ 
src                     └─┘     └─┘
typ                    └─┘   └─┘ 
doc                     └─┘     └─┘
 41  | ⟨f, al⟩ := ⟨some a :: f, λn h, by {cases n with n, contradiction, exact al h}⟩
id                └──┘  └┘                                                └┘ 
src                └──┘   └┘              └────┘ └─────┘  └───────────┘  └────┘  
typ               └──┘  └┘            └────┘└─────┘  └───────────┘  └────┘└┘
doc                                       └────┘ └─────┘  └───────────┘  └────┘  
txt                                       └────┘ └─────┘  └───────────┘  └────┘  
par                                       └────┘ └─────┘  └───────────┘  └────┘  
pid                                             └─────┘                        
st                                      └──────────────┘└─────────────┘└──────────┘└┘
 42  
 43  /-- Get the nth element of a sequence (if it exists) -/
 44  def nth : seq α → ℕ → option α := subtype.val
id             └─┘       └────┘     └─────────┘
src            └─┘        └────┘      └─────────┘
typ            └─┘       └────┘     └─────────┘
doc            └─┘
 45  
 46  /-- A sequence has terminated at position `n` if the value at position `n` equals `none`. -/
 47  def terminated_at (s : seq α) (n : ℕ) : Prop := s.nth n = none
id                          └─┘                    └──┘   └──┘
src                         └─┘                      └──┘    └──┘
typ                         └─┘                    └──┘   └──┘
doc                         └─┘                       └──┘
 48  
 49  /-- It is decidable whether a sequence terminates at a given position. -/
 50  instance terminated_at_decidable (s : seq α) (n : ℕ) : decidable (s.terminated_at n) :=
id                                         └─┘            └───────┘  └────────────┘ 
src                                        └─┘             └───────┘   └────────────┘
typ                                        └─┘            └───────┘  └────────────┘ 
doc                                        └─┘                          └────────────┘
 51  if p : s.nth n = none then is_true p
id   └┘     └──┘   └──┘      └─────┘ 
src  └┘      └──┘    └──┘      └─────┘
typ  └┘     └──┘   └──┘      └─────┘ 
doc          └──┘
 52  else is_false (assume h, by contradiction)
id        └──────┘         
src       └──────┘               └───────────┘
typ       └──────┘              └───────────┘
doc                              └───────────┘
txt                              └───────────┘
par                              └───────────┘
st                              └────────────┘
 53  
 54  /-- A sequence terminates if there is some position `n` at which it has terminated. -/
 55  def terminates (s : seq α) : Prop := ∃ (n : ℕ), s.terminated_at n
id                       └─┘                     └────────────┘ 
src                      └─┘                       └────────────┘
typ                      └─┘                     └────────────┘ 
doc                      └─┘                          └────────────┘
 56  
 57  /-- Functorial action of the functor `option (α × _)` -/
 58  @[simp] def omap (f : β → γ) : option (α × β) → option (α × γ)
id                                └────┘       └────┘    
src                                 └────┘          └────┘    
typ                               └────┘       └────┘    
doc    └──┘
 59  | none          := none
id     └──┘             └──┘
src    └──┘             └──┘
typ    └──┘             └──┘
 60  | (some (a, b)) := some (a, f b)
id      └──┘         └──┘    
src     └──┘           └──┘ 
typ     └──┘         └──┘    
 61  
 62  /-- Get the first element of a sequence -/
 63  def head (s : seq α) : option α := nth s 0
id                 └─┘     └────┘     └─┘ 
src                └─┘      └────┘      └─┘
typ                └─┘     └────┘     └─┘ 
doc                └─┘                  └─┘
 64  
 65  /-- Get the tail of a sequence (or `nil` if the sequence is `nil`) -/
 66  def tail : seq α → seq α
id              └─┘   └─┘ 
src             └─┘     └─┘
typ             └─┘   └─┘ 
doc             └─┘     └─┘
 67  | ⟨f, al⟩ := ⟨f.tail, λ n, al⟩
id        └┘       └───┘    
src                 └───┘
typ       └┘       └───┘    
 68  
 69  protected def mem (a : α) (s : seq α) := some a ∈ s.1
id                                 └─┘      └──┘   
src                                 └─┘       └──┘     
typ                                └─┘      └──┘   
doc                                 └─┘
 70  
 71  instance : has_mem α (seq α) :=
id              └─────┘   └─┘ 
src             └─────┘    └─┘
typ             └─────┘   └─┘ 
doc                        └─┘
 72  ⟨seq.mem⟩
id    └─────┘
src   └─────┘
typ   └─────┘
 73  
 74  theorem le_stable (s : seq α) {m n} (h : m ≤ n) :
id                          └─┘                
src                         └─┘                 
typ                         └─┘                
doc                         └─┘
 75    s.1 m = none → s.1 n = none :=
id         └──┘       └──┘
src          └──┘         └──┘
typ        └──┘       └──┘
 76  by {cases s with f al, induction h with n h IH, exacts [id, λ h2, al (IH h2)]}
id                                                         └┘        └┘  └┘
src      └────┘ └────────┘  └────────┘ └──────────┘  └──────┘└┘└┘ └───┘       └┘
typ      └────┘└────────┘  └────────┘└──────────┘  └──────┘└┘└┘ └───┘└┘ └┘  └┘
doc      └────┘ └────────┘  └────────┘ └──────────┘  └──────┘  └┘ └───┘       └┘
txt      └────┘ └────────┘  └────────┘ └──────────┘  └──────┘  └┘ └───┘       └┘
par      └────┘ └────────┘  └────────┘ └──────────┘  └──────┘  └┘ └───┘       └┘
pid            └────────┘            └─────────┘        └┘  └┘ └───┘       └┘
st     └─────────────────┘└───────────────────────┘└─────────────────────────────┘└┘
 77  
 78  /-- If a sequence terminated at position `n`, it also terminated at `m ≥ n `. -/
 79  lemma terminated_stable {s : seq α} {m n : ℕ} (m_le_n : m ≤ n)
id                                └─┘                        
src                               └─┘                         
typ                               └─┘                        
doc                               └─┘
 80  (terminated_at_m : s.terminated_at m) :
id                      └────────────┘ 
src                      └────────────┘
typ                     └────────────┘ 
doc                      └────────────┘
 81    s.terminated_at n :=
id     └────────────┘ 
src     └────────────┘
typ    └────────────┘ 
doc     └────────────┘
 82  le_stable s m_le_n terminated_at_m
id   └───────┘  └────┘ └─────────────┘
src  └───────┘
typ  └───────┘  └────┘ └─────────────┘
 83  
 84  /--
 85  If `s.nth n = some aₙ` for some value `aₙ`, then there is also some value `aₘ` such
 86  that `s.nth = some aₘ` for `m ≤ n`.
 87  -/
 88  lemma ge_stable (s : seq α) {aₙ : α} {n m : ℕ} (m_le_n : m ≤ n)
id                        └─┘                                
src                       └─┘                                  
typ                       └─┘                                
doc                       └─┘
 89  (s_nth_eq_some : s.nth n = some aₙ) :
id                    └──┘   └──┘ └┘
src                    └──┘    └──┘
typ                   └──┘   └──┘ └┘
doc                    └──┘
 90    ∃ (aₘ : α), s.nth m = some aₘ :=
id              └──┘   └──┘ └┘
src               └──┘    └──┘
typ             └──┘   └──┘ └┘
doc                 └──┘
 91  have s.nth n ≠ none, by simp [s_nth_eq_some],
id        └──┘   └──┘           └───────────┘
src        └──┘    └──┘     └────┘             
typ       └──┘   └──┘     └────┘└───────────┘
doc        └──┘              └────┘             
txt                          └────┘             
par                          └────┘             
pid                                           
st                          └───────────────────┘
 92  have s.nth m ≠ none, from mt (s.le_stable m_le_n) this,
id        └──┘   └──┘       └┘  └────────┘ └────┘  └──┘
src        └──┘    └──┘       └┘   └────────┘
typ       └──┘   └──┘       └┘  └────────┘ └────┘  └──┘
doc        └──┘
 93  with_one.ne_one_iff_exists.elim_left this
id   └────────────────────────┘└────────┘ └──┘
src  └────────────────────────┘└────────┘
typ  └────────────────────────┘└────────┘ └──┘
 94  
 95  theorem not_mem_nil (a : α) : a ∉ @nil α :=
id                                   └─┘ 
src                                    └─┘
typ                                  └─┘ 
doc                                     └─┘
 96  λ ⟨n, (h : some a = none)⟩, by injection h
id             └──┘   └──┘                 
src             └──┘    └──┘       └────────┘ 
typ            └──┘   └──┘       └────────┘
doc                                 └────────┘ 
txt                                 └────────┘ 
par                                 └────────┘ 
pid                                           
st                                 └────────────
 97  
src  
typ  
doc  
txt  
par  
pid  
st   
 98  theorem mem_cons (a : α) : ∀ (s : seq α), a ∈ cons a s
id                                   └─┘      └──┘  
src                                    └─┘        └──┘
typ                                  └─┘      └──┘  
doc                                    └─┘         └──┘
 99  | ⟨f, al⟩ := stream.mem_cons (some a) _
id                └─────────────┘  └──┘ 
src               └─────────────┘  └──┘
typ               └─────────────┘  └──┘ 
100  
101  theorem mem_cons_of_mem (y : α) {a : α} : ∀ {s : seq α}, a ∈ s → a ∈ cons y s
id                                                 └─┘           └──┘  
src                                                   └─┘               └──┘
typ                                                └─┘           └──┘  
doc                                                   └─┘                 └──┘
102  | ⟨f, al⟩ := stream.mem_cons_of_mem (some y)
id                └────────────────────┘  └──┘ 
src               └────────────────────┘  └──┘
typ               └────────────────────┘  └──┘ 
103  
104  theorem eq_or_mem_of_mem_cons {a b : α} : ∀ {s : seq α}, a ∈ cons b s → a = b ∨ a ∈ s
id                                                  └─┘      └──┘           
src                                                   └─┘        └──┘               
typ                                                 └─┘      └──┘           
doc                                                   └─┘         └──┘
105  | ⟨f, al⟩ h := (stream.eq_or_mem_of_mem_cons h).imp_left (λh, by injection h)
id                  └──────────────────────────┘   └──────┘                   
src                  └──────────────────────────┘   └──────┘          └────────┘
typ                 └──────────────────────────┘   └──────┘         └────────┘
doc                                                                   └────────┘
txt                                                                   └────────┘
par                                                                   └────────┘
pid                                                                            
st                                                                   └──────────┘
106  
107  @[simp] theorem mem_cons_iff {a b : α} {s : seq α} : a ∈ cons b s ↔ a = b ∨ a ∈ s :=
id                                              └─┘       └──┘          
src                                              └─┘         └──┘              
typ                                             └─┘       └──┘          
doc    └──┘                                      └─┘          └──┘
108  ⟨eq_or_mem_of_mem_cons, λo, by cases o with e m;
id    └───────────────────┘              
src   └───────────────────┘         └────┘ └───────┘
typ   └───────────────────┘        └────┘└───────┘
doc                                 └────┘ └───────┘
txt                                 └────┘ └───────┘
par                                 └────┘ └───────┘
pid                                       └───────┘
st                                 └──────────────────
109    [{rw e, apply mem_cons}, exact mem_cons_of_mem _ m]⟩
id                 └──────┘         └─────────────┘   
src     └─┘   └────┘└──────┘   └────┘└─────────────┘└─┘
typ     └─┘  └────┘└──────┘   └────┘└─────────────┘└─┘
doc      └─┘   └────┘           └────┘               └─┘
txt      └─┘   └────┘           └────┘               └─┘
par      └─┘   └────┘           └────┘               └─┘
pid                                               └─┘
st   ──┘└───┘└──────────────┘└┘└─────────────────────────┘
110  
111  /-- Destructor for a sequence, resulting in either `none` (for `nil`) or
112    `some (a, s)` (for `cons a s`). -/
113  def destruct (s : seq α) : option (seq1 α) :=
id                     └─┘     └────┘  └──┘ 
src                    └─┘      └────┘  └──┘
typ                    └─┘     └────┘  └──┘ 
doc                    └─┘              └──┘
114  (λa', (a', s.tail)) <$> nth s 0
id     └┘  └┘  └───┘   └─┘ └─┘ 
src             └───┘   └─┘ └─┘
typ    └┘  └┘  └───┘   └─┘ └─┘ 
doc              └───┘       └─┘
115  
116  theorem destruct_eq_nil {s : seq α} : destruct s = none → s = nil :=
id                                └─┘     └──────┘   └──┘     └─┘
src                               └─┘      └──────┘    └──┘      └─┘
typ                               └─┘     └──────┘   └──┘     └─┘
doc                               └─┘      └──────┘                └─┘
117  begin
st   └─────
118    dsimp [destruct],
id            └──────┘
src    └─────┘└──────┘
typ    └─────┘└──────┘
doc    └─────┘└──────┘
txt    └─────┘        
par    └─────┘        
pid                 
st   ─────────────────┘└─
119    induction f0 : nth s 0; intro h,
id                    └─┘ 
src    └────────┘  └─┘└─┘ └┘  └─────┘
typ    └────────┘  └─┘└─┘└┘  └─────┘
doc    └────────┘  └─┘└─┘ └┘  └─────┘
txt    └────────┘  └─┘    └┘  └─────┘
par    └────────┘  └─┘    └┘  └─────┘
pid               └─┘           └┘
st   ────────────────────────────────┘└─
120    { apply subtype.eq,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└──────────────┘└─
121      funext n,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid            └┘
st   ───────────┘└─
122      induction n with n IH, exacts [f0, s.2 IH] },
id                                     └┘     └┘
src      └────────┘ └────────┘  └──────┘  └┘ └─┘  └┘
typ      └────────┘└────────┘  └──────┘└┘└┘└─┘└┘└┘
doc      └────────┘ └────────┘  └──────┘  └┘ └─┘  └┘
txt      └────────┘ └────────┘  └──────┘  └┘ └─┘  └┘
par      └────────┘ └────────┘  └──────┘  └┘ └─┘  └┘
pid                └───────┘        └┘  └┘ └─┘  
st   ────────────────────────┘└────────────────────┘└┘
123    { contradiction }
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid                   
st   ─────────────────┘└─
124  end
st   ──┘
125  
126  theorem destruct_eq_cons {s : seq α} {a s'} : destruct s = some (a, s') → s = cons a s' :=
id                                 └─┘            └──────┘   └──┘   └┘      └──┘  └┘
src                                └─┘             └──────┘    └──┘             └──┘
typ                                └─┘            └──────┘   └──┘   └┘      └──┘  └┘
doc                                └─┘             └──────┘                        └──┘
127  begin
st   └─────
128    dsimp [destruct],
id            └──────┘
src    └─────┘└──────┘
typ    └─────┘└──────┘
doc    └─────┘└──────┘
txt    └─────┘        
par    └─────┘        
pid                 
st   ─────────────────┘└─
129    induction f0 : nth s 0 with a'; intro h,
id                    └─┘ 
src    └────────┘  └─┘└─┘ └────────┘  └─────┘
typ    └────────┘  └─┘└─┘└────────┘  └─────┘
doc    └────────┘  └─┘└─┘ └────────┘  └─────┘
txt    └────────┘  └─┘    └────────┘  └─────┘
par    └────────┘  └─┘    └────────┘  └─────┘
pid               └─┘    └┘└─────┘       └┘
st   ────────────────────────────────────────┘└─
130    { contradiction },
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid                   
st   ───┘└────────────┘└┘
131    { unfold functor.map at h,
src      └─────────────────────┘
typ      └─────────────────────┘
doc      └─────────────────────┘
txt      └─────────────────────┘
par      └─────────────────────┘
pid            └──────────┘└───┘
st   ──────────────────────────┘└─
132      cases s with f al,
id             
src      └────┘ └────────┘
typ      └────┘└────────┘
doc      └────┘ └────────┘
txt      └────┘ └────────┘
par      └────┘ └────────┘
pid            └────────┘
st   ────────────────────┘└─
133      injections with _ h1 h2,
src      └─────────────────────┘
typ      └─────────────────────┘
doc      └─────────────────────┘
txt      └─────────────────────┘
par      └─────────────────────┘
pid                └───────────┘
st   ──────────────────────────┘└─
134      rw ←h2, apply subtype.eq, dsimp [tail, cons],
id           └┘        └────────┘         └──┘  └──┘
src      └──┘    └────┘└────────┘  └─────┘└──┘└┘└──┘
typ      └──┘└┘  └────┘└────────┘  └─────┘└──┘└┘└──┘
doc      └──┘    └────┘            └─────┘└──┘└┘└──┘
txt      └──┘    └────┘            └─────┘    └┘    
par      └──┘    └────┘            └─────┘    └┘    
pid        └┘                              └┘    
st   ─────────┘└────────────────┘└──────────────────┘└─
135      rw h1 at f0, rw ←f0,
id          └┘            └┘
src      └─┘  └────┘  └──┘
typ      └─┘└┘└────┘  └──┘└┘
doc      └─┘  └────┘  └──┘
txt      └─┘  └────┘  └──┘
par      └─┘  └────┘  └──┘
pid          └────┘    └┘
st   ──────────────┘└──────┘└─
136      exact (stream.eta f).symm }
id              └────────┘ 
src      └────┘ └────────┘ └─────┘
typ      └────┘ └────────┘└─────┘
doc      └────┘            └─────┘
txt      └────┘            └─────┘
par      └────┘            └─────┘
pid                       └───┘└┘
st   ─────────────────────────────┘└─
137  end
st   ──┘
138  
139  @[simp] theorem destruct_nil : destruct (nil : seq α) = none := rfl
id                                  └──────┘  └─┘   └─┘    └──┘    └─┘
src                                 └──────┘  └─┘   └─┘     └──┘    └─┘
typ                                 └──────┘  └─┘   └─┘    └──┘    └─┘
doc    └──┘                         └──────┘  └─┘   └─┘
140  
141  @[simp] theorem destruct_cons (a : α) : ∀ s, destruct (cons a s) = some (a, s)
id                                              └──────┘  └──┘     └──┘   
src                                               └──────┘  └──┘       └──┘ 
typ                                             └──────┘  └──┘     └──┘   
doc    └──┘                                       └──────┘  └──┘
142  | ⟨f, al⟩ := begin
st                └─────
143    unfold cons destruct functor.map,
src    └──────────────────────────────┘
typ    └──────────────────────────────┘
doc    └──────────────────────────────┘
txt    └──────────────────────────────┘
par    └──────────────────────────────┘
pid          └────────────────────────┘
st   ─────────────────────────────────┘└─
144    apply congr_arg (λ s, some (a, s)),
id           └───────┘       └──┘ 
src    └────┘└───────┘  └──┘└──┘ └┘ └┘
typ    └────┘└───────┘  └──┘└──┘└┘ └┘
doc    └────┘           └──┘      └┘ └┘
txt    └────┘           └──┘      └┘ └┘
par    └────┘           └──┘      └┘ └┘
pid                    └──┘      └┘ └┘
st   ───────────────────────────────────┘└─
145    apply subtype.eq, dsimp [tail], rw [stream.tail_cons]
id           └────────┘         └──┘       └──────────────┘
src    └────┘└────────┘  └─────┘└──┘  └──┘└──────────────┘└┘
typ    └────┘└────────┘  └─────┘└──┘  └──┘└──────────────┘└┘
doc    └────┘            └─────┘└──┘  └──┘                └┘
txt    └────┘            └─────┘      └──┘                └┘
par    └────┘            └─────┘      └──┘                └┘
pid                                  └┘                
st   ─────────────────┘└────────────┘└────────────────────┘
146  end
st   └─┘
147  
148  theorem head_eq_destruct (s : seq α) : head s = prod.fst <$> destruct s :=
id                                 └─┘     └──┘   └──────┘ └─┘ └──────┘ 
src                                └─┘      └──┘    └──────┘ └─┘ └──────┘
typ                                └─┘     └──┘   └──────┘ └─┘ └──────┘ 
doc                                └─┘      └──┘                  └──────┘
149  by unfold destruct head; cases nth s 0; refl
id                                  └─┘ 
src     └──────────────────┘  └────┘└─┘ └┘  └────
typ     └──────────────────┘  └────┘└─┘└┘  └────
doc     └──────────────────┘  └────┘└─┘ └┘  └────
txt     └──────────────────┘  └────┘    └┘  └────
par     └──────────────────┘  └────┘    └┘  └────
pid           └────────────┘                 
st     └──────────────────────────────────────────
150  
src  
typ  
doc  
txt  
par  
pid  
st   
151  @[simp] theorem head_nil : head (nil : seq α) = none := rfl
id                              └──┘  └─┘   └─┘    └──┘    └─┘
src                             └──┘  └─┘   └─┘     └──┘    └─┘
typ                             └──┘  └─┘   └─┘    └──┘    └─┘
doc    └──┘                     └──┘  └─┘   └─┘
152  
153  @[simp] theorem head_cons (a : α) (s) : head (cons a s) = some a :=
id                                          └──┘  └──┘     └──┘ 
src                                          └──┘  └──┘       └──┘
typ                                         └──┘  └──┘     └──┘ 
doc    └──┘                                  └──┘  └──┘
154  by rw [head_eq_destruct, destruct_cons]; refl
id          └──────────────┘  └───────────┘
src     └──┘└──────────────┘└┘└───────────┘  └────
typ     └──┘└──────────────┘└┘└───────────┘  └────
doc     └──┘                └┘               └────
txt     └──┘                └┘               └────
par     └──┘                └┘               └────
pid       └┘                └┘                   
st     └───────────────────┘└─────────────┘└──────
155  
src  
typ  
doc  
txt  
par  
pid  
st   
156  @[simp] theorem tail_nil : tail (nil : seq α) = nil := rfl
id                              └──┘  └─┘   └─┘    └─┘    └─┘
src                             └──┘  └─┘   └─┘     └─┘    └─┘
typ                             └──┘  └─┘   └─┘    └─┘    └─┘
doc    └──┘                     └──┘  └─┘   └─┘      └─┘
157  
158  @[simp] theorem tail_cons (a : α) (s) : tail (cons a s) = s :=
id                                          └──┘  └──┘     
src                                          └──┘  └──┘      
typ                                         └──┘  └──┘     
doc    └──┘                                  └──┘  └──┘
159  by cases s with f al; apply subtype.eq; dsimp [tail, cons]; rw [stream.tail_cons]
id                              └────────┘         └──┘  └──┘       └──────────────┘
src     └────┘ └────────┘  └────┘└────────┘  └─────┘└──┘└┘└──┘  └──┘└──────────────┘└─
typ     └────┘└────────┘  └────┘└────────┘  └─────┘└──┘└┘└──┘  └──┘└──────────────┘└─
doc     └────┘ └────────┘  └────┘            └─────┘└──┘└┘└──┘  └──┘                └─
txt     └────┘ └────────┘  └────┘            └─────┘    └┘      └──┘                └─
par     └────┘ └────────┘  └────┘            └─────┘    └┘      └──┘                └─
pid           └────────┘                            └┘        └┘                
st     └────────────────────────────────────────────────────────────┘└──────────────┘
160  
src  
typ  
doc  
txt  
par  
pid  
st   
161  def cases_on {C : seq α → Sort v} (s : seq α)
id                     └─┘                 └─┘ 
src                    └─┘                  └─┘
typ                    └─┘                 └─┘ 
doc                    └─┘                  └─┘
162    (h1 : C nil) (h2 : ∀ x s, C (cons x s)) : C s := begin
id            └─┘               └──┘        
src            └─┘                  └──┘
typ           └─┘               └──┘        
doc            └─┘                  └──┘
st                                                      └─────
163    induction H : destruct s with v v,
id                   └──────┘ 
src    └────────┘ └─┘└──────┘ └───────┘
typ    └────────┘ └─┘└──────┘└───────┘
doc    └────────┘ └─┘└──────┘ └───────┘
txt    └────────┘ └─┘         └───────┘
par    └────────┘ └─┘         └───────┘
pid              └─┘         └──────┘
st   ──────────────────────────────────┘└─
164    { rw destruct_eq_nil H, apply h1 },
id          └─────────────┘ 
src      └─┘└─────────────┘   └────┘  
typ      └─┘└─────────────┘  └────┘  
doc      └─┘                  └────┘  
txt      └─┘                  └────┘  
par      └─┘                  └────┘  
pid                                 
st   ───┘└──────────────────┘└─────────┘└┘
165    { cases v with a s', rw destruct_eq_cons H, apply h2 }
id                            └──────────────┘ 
src      └────┘ └────────┘  └─┘└──────────────┘   └────┘  
typ      └────┘└────────┘  └─┘└──────────────┘  └────┘  
doc      └────┘ └────────┘  └─┘                   └────┘  
txt      └────┘ └────────┘  └─┘                   └────┘  
par      └────┘ └────────┘  └─┘                   └────┘  
pid            └────────┘                              
st   ────────────────────┘└─────────────────────┘└─────────┘└─
166  end
st   ──┘
167  
168  theorem mem_rec_on {C : seq α → Prop} {a s} (M : a ∈ s)
id                           └─┘                       
src                          └─┘                        
typ                          └─┘                       
doc                          └─┘
169    (h1 : ∀ b s', (a = b ∨ C s') → C (cons b s')) : C s :=
id              └┘        └┘      └──┘  └┘      
src                                    └──┘
typ             └┘        └┘      └──┘  └┘      
doc                                      └──┘
170  begin
st   └─────
171    cases M with k e, unfold stream.nth at e,
id           
src    └────┘ └───────┘  └────────────────────┘
typ    └────┘└───────┘  └────────────────────┘
doc    └────┘ └───────┘  └────────────────────┘
txt    └────┘ └───────┘  └────────────────────┘
par    └────┘ └───────┘  └────────────────────┘
pid          └───────┘        └─────────┘└───┘
st   ─────────────────┘└──────────────────────┘└─
172    induction k with k IH generalizing s,
id               
src    └────────┘ └───────────────────────┘
typ    └────────┘└───────────────────────┘
doc    └────────┘ └───────────────────────┘
txt    └────────┘ └───────────────────────┘
par    └────────┘ └───────────────────────┘
pid              └───────┘└─────────────┘
st   ─────────────────────────────────────┘└─
173    { have TH : s = cons a (tail s),
id                    └──┘   └──┘ 
src      └────────┘ └──┘  └──┘ 
typ      └────────┘ └──┘ └──┘
doc      └────────┘  └──┘  └──┘ 
txt      └────────┘             
par      └────────┘             
pid      └─────┘└─┘             
st   ───┘└───────────────────────────┘└─
174      { apply destruct_eq_cons,
id               └──────────────┘
src        └────┘└──────────────┘
typ        └────┘└──────────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────┘└────────────────────┘└─
175        unfold destruct nth functor.map, rw ←e, refl },
id                                              
src        └─────────────────────────────┘  └──┘   └───┘
typ        └─────────────────────────────┘  └──┘  └───┘
doc        └─────────────────────────────┘  └──┘   └───┘
txt        └─────────────────────────────┘  └──┘   └───┘
par        └─────────────────────────────┘  └──┘   └───┘
pid              └───────────────────────┘    └┘       
st   ────────────────────────────────────┘└─────┘└─────┘└┘
176      rw TH, apply h1 _ _ (or.inl rfl) },
id          └┘        └┘      └────┘ └─┘
src      └─┘    └────┘  └───┘ └────┘└─┘└┘
typ      └─┘└┘  └────┘└┘└───┘ └────┘└─┘└┘
doc      └─┘    └────┘  └───┘          └┘
txt      └─┘    └────┘  └───┘          └┘
par      └─┘    └────┘  └───┘          └┘
pid                   └───┘          
st   ────────┘└──────────────────────────┘└┘
177    revert e, apply s.cases_on _ (λ b s', _); intro e,
id                     └────────┘
src    └──────┘  └────┘└────────┘└─┘  └───────┘  └─────┘
typ    └──────┘  └────┘└────────┘└─┘  └───────┘  └─────┘
doc    └──────┘  └────┘          └─┘  └───────┘  └─────┘
txt    └──────┘  └────┘          └─┘  └───────┘  └─────┘
par    └──────┘  └────┘          └─┘  └───────┘  └─────┘
pid          └┘                 └─┘  └───────┘       └┘
st   ─────────┘└───────────────────────────────────────┘└─
178    { injection e },
id                 
src      └────────┘ 
typ      └────────┘
doc      └────────┘ 
txt      └────────┘ 
par      └────────┘ 
pid                
st   ───┘└──────────┘└┘
179    { have h_eq : (cons b s').val (nat.succ k) = s'.val k, { cases s'; refl },
id                    └──┘           └──────┘      └────┘           └┘
src      └──────────┘ └──┘   └────┘ └──────┘ └┘ └────┘     └────┘    └───┘
typ      └──────────┘ └──┘  └────┘ └──────┘ └┘ └────┘    └────┘└┘  └───┘
doc      └──────────┘ └──┘   └────┘          └┘            └────┘    └───┘
txt      └──────────┘        └────┘          └┘            └────┘    └───┘
par      └──────────┘        └────┘          └┘            └────┘    └───┘
pid      └───────┘└─┘        └────┘          └┘                         
st   ──────────────────────────────────────────────────────┘└──┘└─────────────┘└┘
180      rw [h_eq] at e,
id           └──┘
src      └──┘    └────┘
typ      └──┘└──┘└────┘
doc      └──┘    └────┘
txt      └──┘    └────┘
par      └──┘    └────┘
pid        └┘    └───┘
st   ───────────┘└───┘└─
181      apply h1 _ _ (or.inr (IH e)) }
id             └┘      └────┘  └┘ 
src      └────┘  └───┘ └────┘    └─┘
typ      └────┘└┘└───┘ └────┘ └┘└─┘
doc      └────┘  └───┘           └─┘
txt      └────┘  └───┘           └─┘
par      └────┘  └───┘           └─┘
pid             └───┘           └┘
st   ────────────────────────────────┘└─
182  end
st   ──┘
183  
184  def corec.F (f : β → option (α × β)) : option β → option α × option β
id                       └────┘         └────┘   └────┘   └────┘ 
src                       └────┘           └────┘     └────┘    └────┘
typ                      └────┘         └────┘   └────┘   └────┘ 
185  | none     := (none, none)
id     └──┘        └──┘  └──┘
src    └──┘        └──┘  └──┘
typ    └──┘        └──┘  └──┘
186  | (some b) := match f b with none := (none, none) | some (a, b') := (some a, some b') end
id      └──┘                    └──┘    └──┘  └──┘    └──┘   └┘     └──┘    └──┘
src     └──┘                      └──┘    └──┘  └──┘    └──┘           └──┘    └──┘
typ     └──┘                    └──┘    └──┘  └──┘    └──┘   └┘     └──┘    └──┘
187  
188  /-- Corecursor for `seq α` as a coinductive type. Iterates `f` to produce new elements
189    of the sequence until `none` is obtained. -/
190  def corec (f : β → option (α × β)) (b : β) : seq α :=
id                     └────┘                └─┘ 
src                     └────┘                   └─┘
typ                    └────┘                └─┘ 
doc                                               └─┘
191  begin
st   └─────
192    refine ⟨stream.corec' (corec.F f) (some b), λn h, _⟩,
id             └───────────┘  └─────┘    └──┘ 
src    └─────┘ └───────────┘ └─────┘ └┘ └──┘ └─┘ └─────┘
typ    └─────┘ └───────────┘ └─────┘└┘ └──┘└─┘ └─────┘
doc    └─────┘                       └┘      └─┘ └─────┘
txt    └─────┘                       └┘      └─┘ └─────┘
par    └─────┘                       └┘      └─┘ └─────┘
pid                                 └┘      └─┘ └─────┘
st   ─────────────────────────────────────────────────────┘└─
193    rw stream.corec'_eq,
id        └──────────────┘
src    └─┘└──────────────┘
typ    └─┘└──────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────────────────┘└─
194    change stream.corec' (corec.F f) (corec.F f (some b)).2 n = none,
id            └───────────┘              └─────┘   └──┘        └──┘
src    └─────┘└───────────┘         └┘ └─────┘  └──┘ └───┘ └──┘
typ    └─────┘└───────────┘         └┘ └─────┘ └──┘└───┘└──┘
doc    └─────┘                      └┘               └───┘  
txt    └─────┘                      └┘               └───┘  
par    └─────┘                      └┘               └───┘  
pid                                └┘               └───┘  
st   ─────────────────────────────────────────────────────────────────┘└─
195    revert h, generalize : some b = o, revert o,
id                            └──┘ 
src    └──────┘  └───────────┘└──┘     └──────┘
typ    └──────┘  └───────────┘└──┘    └──────┘
doc    └──────┘  └───────────┘         └──────┘
txt    └──────┘  └───────────┘         └──────┘
par    └──────┘  └───────────┘         └──────┘
pid          └┘                           └┘
st   ─────────┘└───────────────────────┘└────────┘└─
196    induction n with n IH; intro o,
id               
src    └────────┘ └────────┘  └─────┘
typ    └────────┘└────────┘  └─────┘
doc    └────────┘ └────────┘  └─────┘
txt    └────────┘ └────────┘  └─────┘
par    └────────┘ └────────┘  └─────┘
pid              └───────┘       └┘
st   ───────────────────────────────┘└─
197    { change (corec.F f o).1 = none → (corec.F f (corec.F f o).2).1 = none,
id                                                  └─────┘           └──┘
src      └─────┘          └──┘                └─────┘  └─────┘ └──┘
typ      └─────┘          └──┘               └─────┘└─────┘ └──┘
doc      └─────┘          └──┘                         └─────┘ 
txt      └─────┘          └──┘                         └─────┘ 
par      └─────┘          └──┘                         └─────┘ 
pid                      └──┘                         └─────┘ 
st   ───┘└──────────────────────────────────────────────────────────────────┘└─
198      cases o with b; intro h, { refl },
id             
src      └────┘ └─────┘  └─────┘    └───┘
typ      └────┘└─────┘  └─────┘    └───┘
doc      └────┘ └─────┘  └─────┘    └───┘
txt      └────┘ └─────┘  └─────┘    └───┘
par      └────┘ └─────┘  └─────┘    └───┘
pid            └─────┘       └┘        
st   ──────────────────────────┘└──┘└───┘└┘
199      dsimp [corec.F] at h, dsimp [corec.F],
id              └─────┘               └─────┘
src      └─────┘└─────┘└────┘  └─────┘└─────┘
typ      └─────┘└─────┘└────┘  └─────┘└─────┘
doc      └─────┘       └────┘  └─────┘       
txt      └─────┘       └────┘  └─────┘       
par      └─────┘       └────┘  └─────┘       
pid                  └──┘              
st   ───────────────────────┘└───────────────┘└─
200      cases f b with s, { refl },
id              
src      └────┘  └─────┘    └───┘
typ      └────┘└─────┘    └───┘
doc      └────┘  └─────┘    └───┘
txt      └────┘  └─────┘    └───┘
par      └────┘  └─────┘    └───┘
pid             └─────┘        
st   ───────────────────┘└──┘└───┘└┘
201      { cases s with a b', contradiction } },
id               
src        └────┘ └────────┘  └────────────┘
typ        └────┘└────────┘  └────────────┘
doc        └────┘ └────────┘  └────────────┘
txt        └────┘ └────────┘  └────────────┘
par        └────┘ └────────┘  └────────────┘
pid              └────────┘               
st   ──────────────────────┘└──────────────┘└──┘
202    { rw [stream.corec'_eq (corec.F f) (corec.F f o).2,
id           └──────────────┘              └─────┘  
src      └──┘└──────────────┘         └┘ └─────┘  └────
typ      └──┘└──────────────┘         └┘ └─────┘└────
doc      └──┘                         └┘          └────
txt      └──┘                         └┘          └────
par      └──┘                         └┘          └────
pid        └┘                         └┘          └────
st   ─────────────────────────────────────────────────┘└───
203          stream.corec'_eq (corec.F f) o],
id           └──────────────┘  └─────┘   
src  ───────┘└──────────────┘ └─────┘ └┘ 
typ  ───────┘└──────────────┘ └─────┘└┘
doc  ───────┘                         └┘ 
txt  ───────┘                         └┘ 
par  ───────┘                         └┘ 
pid  ───────┘                         └┘ 
st   ─────────────────────────────────────┘└─
204      exact IH (corec.F f o).2 }
id             └┘  └─────┘  
src      └────┘   └─────┘  └──┘
typ      └────┘└┘ └─────┘└──┘
doc      └────┘            └──┘
txt      └────┘            └──┘
par      └────┘            └──┘
pid                       └─┘
st   ────────────────────────────┘└─
205  end
st   ──┘
206  
207  @[simp] theorem corec_eq (f : β → option (α × β)) (b : β) :
id                                    └────┘            
src                                    └────┘    
typ                                   └────┘            
doc    └──┘
208    destruct (corec f b) = omap (corec f) (f b) :=
id     └──────┘  └───┘     └──┘  └───┘     
src    └──────┘  └───┘       └──┘  └───┘
typ    └──────┘  └───┘     └──┘  └───┘     
doc    └──────┘  └───┘        └──┘  └───┘
209  begin
st   └─────
210    dsimp [corec, destruct, nth],
id            └───┘  └──────┘  └─┘
src    └─────┘└───┘└┘└──────┘└┘└─┘
typ    └─────┘└───┘└┘└──────┘└┘└─┘
doc    └─────┘└───┘└┘└──────┘└┘└─┘
txt    └─────┘     └┘        └┘   
par    └─────┘     └┘        └┘   
pid              └┘        └┘   
st   ─────────────────────────────┘└─
211    change stream.corec' (corec.F f) (some b) 0 with (corec.F f (some b)).1,
id            └───────────┘  └─────┘    └──┘           └─────┘   └──┘ 
src    └─────┘└───────────┘ └─────┘ └┘ └──┘ └───────┘ └─────┘  └──┘ └──┘
typ    └─────┘└───────────┘ └─────┘└┘ └──┘└───────┘ └─────┘ └──┘└──┘
doc    └─────┘                      └┘      └───────┘               └──┘
txt    └─────┘                      └┘      └───────┘               └──┘
par    └─────┘                      └┘      └───────┘               └──┘
pid                                └┘      └┘└─────┘               └┘└┘
st   ────────────────────────────────────────────────────────────────────────┘└─
212    unfold functor.map, dsimp [corec.F],
id                                └─────┘
src    └────────────────┘  └─────┘└─────┘
typ    └────────────────┘  └─────┘└─────┘
doc    └────────────────┘  └─────┘       
txt    └────────────────┘  └─────┘       
par    └────────────────┘  └─────┘       
pid          └──────────┘              
st   ───────────────────┘└───────────────┘└─
213    induction h : f b with s, { refl },
id                    
src    └────────┘ └─┘  └─────┘    └───┘
typ    └────────┘ └─┘└─────┘    └───┘
doc    └────────┘ └─┘  └─────┘    └───┘
txt    └────────┘ └─┘  └─────┘    └───┘
par    └────────┘ └─┘  └─────┘    └───┘
pid              └─┘  └────┘        
st   ─────────────────────────┘└──┘└───┘└┘
214    cases s with a b', dsimp [corec.F],
id                              └─────┘
src    └────┘ └────────┘  └─────┘└─────┘
typ    └────┘└────────┘  └─────┘└─────┘
doc    └────┘ └────────┘  └─────┘       
txt    └────┘ └────────┘  └─────┘       
par    └────┘ └────────┘  └─────┘       
pid          └────────┘              
st   ──────────────────┘└───────────────┘└─
215    apply congr_arg (λ b', some (a, b')),
id           └───────┘        └──┘ 
src    └────┘└───────┘  └───┘└──┘ └┘  └┘
typ    └────┘└───────┘  └───┘└──┘└┘  └┘
doc    └────┘           └───┘      └┘  └┘
txt    └────┘           └───┘      └┘  └┘
par    └────┘           └───┘      └┘  └┘
pid                    └───┘      └┘  └┘
st   ─────────────────────────────────────┘└─
216    apply subtype.eq,
id           └────────┘
src    └────┘└────────┘
typ    └────┘└────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────┘└─
217    dsimp [corec, tail],
id            └───┘  └──┘
src    └─────┘└───┘└┘└──┘
typ    └─────┘└───┘└┘└──┘
doc    └─────┘└───┘└┘└──┘
txt    └─────┘     └┘    
par    └─────┘     └┘    
pid              └┘    
st   ────────────────────┘└─
218    rw [stream.corec'_eq, stream.tail_cons],
id         └──────────────┘  └──────────────┘
src    └──┘└──────────────┘└┘└──────────────┘
typ    └──┘└──────────────┘└┘└──────────────┘
doc    └──┘                └┘                
txt    └──┘                └┘                
par    └──┘                └┘                
pid      └┘                └┘                
st   ─────────────────────┘└────────────────┘└──
219    dsimp [corec.F], rw h, refl
id            └─────┘      
src    └─────┘└─────┘  └─┘   └───┘
typ    └─────┘└─────┘  └─┘  └───┘
doc    └─────┘         └─┘   └───┘
txt    └─────┘         └─┘   └───┘
par    └─────┘         └─┘   └───┘
pid                           
st   ────────────────┘└────┘└─────┘
220  end
st   └─┘
221  
222  /-- Embed a list as a sequence -/
223  def of_list (l : list α) : seq α :=
id                    └──┘     └─┘ 
src                   └──┘      └─┘
typ                   └──┘     └─┘ 
doc                             └─┘
224  ⟨list.nth l, λn h, begin
id    └──────┘     
src   └──────┘
typ   └──────┘     
st                      └─────
225    induction l with a l IH generalizing n, refl,
id               
src    └────────┘ └─────────────────────────┘  └──┘
typ    └────────┘└─────────────────────────┘  └──┘
doc    └────────┘ └─────────────────────────┘  └──┘
txt    └────────┘ └─────────────────────────┘  └──┘
par    └────────┘ └─────────────────────────┘  └──┘
pid              └─────────┘└─────────────┘
st   ───────────────────────────────────────┘└────┘└─
226    dsimp [list.nth], cases n with n; dsimp [list.nth] at h,
id            └──────┘                         └──────┘
src    └─────┘└──────┘  └────┘ └─────┘  └─────┘└──────┘└────┘
typ    └─────┘└──────┘  └────┘└─────┘  └─────┘└──────┘└────┘
doc    └─────┘          └────┘ └─────┘  └─────┘        └────┘
txt    └─────┘          └────┘ └─────┘  └─────┘        └────┘
par    └─────┘          └────┘ └─────┘  └─────┘        └────┘
pid                         └─────┘               └──┘
st   ─────────────────┘└─────────────────────────────────────┘└─
227    { contradiction },
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid                   
st   ───┘└────────────┘└┘
228    { apply IH _ h }
id             └┘   
src      └────┘  └─┘ 
typ      └────┘└┘└─┘
doc      └────┘  └─┘ 
txt      └────┘  └─┘ 
par      └────┘  └─┘ 
pid             └─┘ 
st   ────────────────┘└─
229  end⟩
st   ──┘
230  
231  instance coe_list : has_coe (list α) (seq α) := ⟨of_list⟩
id                       └─────┘  └──┘    └─┘       └─────┘
src                      └─────┘  └──┘     └─┘        └─────┘
typ                      └─────┘  └──┘    └─┘       └─────┘
doc                                        └─┘        └─────┘
232  
233  section bisim
234    variable (R : seq α → seq α → Prop)
id                   └─┘     └─┘
src                  └─┘     └─┘
typ                  └─┘     └─┘
doc                  └─┘     └─┘
235  
236    local infix ~ := R
237  
238    def bisim_o : option (seq1 α) → option (seq1 α) → Prop
id                   └────┘  └──┘    └────┘  └──┘ 
src                  └────┘  └──┘      └────┘  └──┘
typ                  └────┘  └──┘    └────┘  └──┘ 
doc                          └──┘              └──┘
239    | none          none            := true
id                     └──┘               └──┘
src                    └──┘               └──┘
typ                    └──┘               └──┘
240    | (some (a, s)) (some (a', s')) := a = a' ∧ R s s'
id                   └──┘ └┘  └┘             
src                    └──┘                   
typ                  └──┘ └┘  └┘             
241    | _             _               := false
id                                        └───┘
src                                       └───┘
typ                                       └───┘
242    attribute [simp] bisim_o
id                      └─────┘
src                     └─────┘
typ                     └─────┘
doc               └──┘
243  
244    def is_bisimulation := ∀ ⦃s₁ s₂⦄, s₁ ~ s₂ → bisim_o R (destruct s₁) (destruct s₂)
id                               └┘ └┘   └┘  └┘   └─────┘   └──────┘ └┘   └──────┘ └┘
src                                                └─────┘    └──────┘      └──────┘
typ                              └┘ └┘   └┘  └┘   └─────┘   └──────┘ └┘   └──────┘ └┘
doc                                                           └──────┘      └──────┘
245  
246    -- If two streams are bisimilar, then they are equal
247    theorem eq_of_bisim (bisim : is_bisimulation R) {s₁ s₂} (r : s₁ ~ s₂) : s₁ = s₂ :=
id                                  └─────────────┘                └┘  └┘    └┘  └┘
src                                 └─────────────┘                               
typ                                 └─────────────┘                └┘  └┘    └┘  └┘
248    begin
st     └─────
249      apply subtype.eq,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────┘└─
250      apply stream.eq_of_bisim (λx y, ∃ s s' : seq α, s.1 = x ∧ s'.1 = y ∧ R s s'),
id             └────────────────┘                └─┘                     
src      └────┘└────────────────┘  └───┘└──────┘└─┘  └─┘   └─┘       
typ      └────┘└────────────────┘  └───┘└──────┘└─┘ └─┘   └─┘      
doc      └────┘                    └───┘ └──────┘└─┘   └─┘     └─┘       
txt      └────┘                    └───┘ └──────┘      └─┘     └─┘       
par      └────┘                    └───┘ └──────┘      └─┘     └─┘       
pid                               └───┘ └──────┘      └─┘     └─┘       
st   ───────────────────────────────────────────────────────────────────────────────┘└─
251      dsimp [stream.is_bisimulation],
id              └────────────────────┘
src      └─────┘└────────────────────┘
typ      └─────┘└────────────────────┘
doc      └─────┘                      
txt      └─────┘                      
par      └─────┘                      
pid                                 
st   ─────────────────────────────────┘└─
252      intros t₁ t₂ e,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid            └──────┘
st   ─────────────────┘└─
253      exact match t₁, t₂, e with ._, ._, ⟨s, s', rfl, rfl, r⟩ :=
id                   └┘  └┘                   └┘       └─┘
src      └────┘       └┘  └┘ └────┘  └┘  └┘  └┘  └┘   └┘└─┘└┘ └────
typ      └────┘     └┘└┘└┘└┘└────┘  └┘  └┘ └┘└┘└┘   └┘└─┘└┘ └────
doc      └────┘       └┘  └┘ └────┘  └┘  └┘  └┘  └┘   └┘   └┘ └────
txt      └────┘       └┘  └┘ └────┘  └┘  └┘  └┘  └┘   └┘   └┘ └────
par      └────┘       └┘  └┘ └────┘  └┘  └┘  └┘  └┘   └┘   └┘ └────
pid                  └┘  └┘ └────┘  └┘  └┘  └┘  └┘   └┘   └┘ └────
st   ───────────────────────────────────────────────────────────────
254        suffices head s = head s' ∧ R (tail s) (tail s'), from
id                           └──┘      
src  ─────┘        └────┘  └──┘          └┘       └───────
typ  ─────┘        └────┘  └──┘         └┘       └───────
doc  ─────┘        └────┘  └──┘          └┘       └───────
txt  ─────┘        └────┘                └┘       └───────
par  ─────┘        └────┘                └┘       └───────
pid  ─────┘        └────┘                └┘       └───────
st   ─────────────────────────────────────────────────────────────
255        and.imp id (λr, ⟨tail s, tail s',
id         └─────┘ └┘               └──┘
src  ─────┘└─────┘└┘  └─┘      └┘└──┘  └─
typ  ─────┘└─────┘└┘  └─┘      └┘└──┘  └─
doc  ─────┘           └─┘      └┘└──┘  └─
txt  ─────┘           └─┘      └┘      └─
par  ─────┘           └─┘      └┘      └─
pid  ─────┘           └─┘      └┘      └─
st   ────────────────────────────────────────
256          by cases s; refl, by cases s'; refl, r⟩) this,
id                                     └┘
src  ───────┘  └────┘ └┘└──┘└┘  └────┘  └┘└──┘└┘ └─┘    └─
typ  ───────┘  └────┘└┘└──┘└┘  └────┘└┘└┘└──┘└┘ └─┘    └─
doc  ───────┘  └────┘ └┘└──┘└┘  └────┘  └┘└──┘└┘ └─┘    └─
txt  ───────┘  └────┘ └┘└──┘└┘  └────┘  └┘└──┘└┘ └─┘    └─
par  ───────┘  └────┘ └┘└──┘└┘  └────┘  └┘└──┘└┘ └─┘    └─
pid  ───────┘  └─────┘ └──────┘  └─────┘  └──────┘ └─┘    └─
st   ─────────┘└────────────┘└──┘└─────────────┘└───────────
257        begin
src  ─────┘     
typ  ─────┘     
doc  ─────┘     
txt  ─────┘     
par  ─────┘     
pid  ─────┘     
st   ─────┘└─────
258          have := bisim r, revert r this,
id                   └───┘ 
src  ───────┘└──────┘      └┘└───────────┘└─
typ  ───────┘└──────┘└───┘└┘└───────────┘└─
doc  ───────┘└──────┘      └┘└───────────┘└─
txt  ───────┘└──────┘      └┘└───────────┘└─
par  ───────┘└──────┘      └┘└───────────┘└─
pid  ───────────────┘      └────────────────
st   ──────────────────────┘└─────────────┘└─
259          apply cases_on s _ _; intros; apply cases_on s' _ _; intros; intros r this,
id                 └──────┘                     └──────┘ └┘
src  ───────┘└────┘└──────┘ └──┘└┘└────┘└┘└────┘└──────┘  └──┘└┘└────┘└┘└───────────┘└─
typ  ─────────────┘└──────┘└────┘└────┘└──────┘└──────┘└┘└────┘└────┘└┘└───────────┘└─
doc  ───────┘└────┘         └──┘└┘└────┘└┘└────┘          └──┘└┘└────┘└┘└───────────┘└─
txt  ───────┘└────┘         └──┘└┘└────┘└┘└────┘          └──┘└┘└────┘└┘└───────────┘└─
par  ─────────────┘         └────┘└────┘└──────┘          └────┘└────┘└┘└───────────┘└─
pid  ─────────────┘         └──────────────────┘          └────────────────────────────
st   ─────────────────────────────────────────────────────────────────────────────────┘└─
260          { constructor, refl, assumption },
src  ─────────┘└─────────┘└┘└──┘└┘└─────────┘└──
typ  ─────────┘└─────────┘└┘└──┘└┘└─────────┘└──
doc  ─────────┘└─────────┘└┘└──┘└┘└─────────┘└──
txt  ─────────┘└─────────┘└┘└──┘└┘└─────────┘└──
par  ─────────┘└─────────┘└┘└──┘└┘└─────────┘└──
pid  ───────────────────────────────────────────
st   ────────┘└──────────┘└────┘└───────────┘└─
261          { rw [destruct_nil, destruct_cons] at this,
id                 └──────────┘  └───────────┘
src  ─────────┘└──┘└──────────┘└┘└───────────┘└───────┘└─
typ  ─────────┘└──┘└──────────┘└┘└───────────┘└───────┘└─
doc  ─────────┘└──┘            └┘             └───────┘└─
txt  ─────────┘└──┘            └┘             └───────┘└─
par  ─────────┘└──┘            └┘             └───────┘└─
pid  ─────────────┘            └┘             └──────────
st   ────────┘└───────────────┘└─────────────┘└──────┘└─
262            exact false.elim this },
id                   └────────┘ └──┘
src  ───────────────┘└────────┘    └───
typ  ───────────────┘└────────┘└──┘└───
doc  ───────────────┘              └───
txt  ───────────────┘              └───
par  ───────────────┘              └───
pid  ───────────────┘              └───
st   ───────────────────────────────┘└─
263          { rw [destruct_nil, destruct_cons] at this,
id                 └──────────┘  └───────────┘
src  ─────────┘└──┘└──────────┘└┘└───────────┘└───────┘└─
typ  ─────────┘└──┘└──────────┘└┘└───────────┘└───────┘└─
doc  ─────────┘└──┘            └┘             └───────┘└─
txt  ─────────┘└──┘            └┘             └───────┘└─
par  ─────────┘└──┘            └┘             └───────┘└─
pid  ─────────────┘            └┘             └──────────
st   ────────┘└───────────────┘└─────────────┘└──────┘└─
264            exact false.elim this },
id                   └────────┘ └──┘
src  ───────────────┘└────────┘    └───
typ  ───────────────┘└────────┘└──┘└───
doc  ───────────────┘              └───
txt  ───────────────┘              └───
par  ───────────────┘              └───
pid  ───────────────┘              └───
st   ───────────────────────────────┘└─
265          { rw [destruct_cons, destruct_cons] at this,
id                 └───────────┘  └───────────┘
src  ─────────┘└──┘└───────────┘└┘└───────────┘└───────┘└─
typ  ─────────┘└──┘└───────────┘└┘└───────────┘└───────┘└─
doc  ─────────┘└──┘             └┘             └───────┘└─
txt  ─────────┘└──┘             └┘             └───────┘└─
par  ─────────┘└──┘             └┘             └───────┘└─
pid  ─────────────┘             └┘             └──────────
st   ──────────────────────────┘└─────────────┘└──────┘└─
266            rw [head_cons, head_cons, tail_cons, tail_cons],
id                 └───────┘  └───────┘  └───────┘  └───────┘
src  ─────────┘└──┘└───────┘└┘└───────┘└┘└───────┘└┘└───────┘└─
typ  ─────────┘└──┘└───────┘└┘└───────┘└┘└───────┘└┘└───────┘└─
doc  ─────────┘└──┘         └┘         └┘         └┘         └─
txt  ─────────┘└──┘         └┘         └┘         └┘         └─
par  ─────────┘└──┘         └┘         └┘         └┘         └─
pid  ─────────────┘         └┘         └┘         └┘         └──
st   ──────────────────────┘└─────────┘└─────────┘└─────────┘└──
267            cases this with h1 h2,
id                   └──┘
src  ─────────┘└────┘    └─────────┘└─
typ  ─────────┘└────┘└──┘└─────────┘└─
doc  ─────────┘└────┘    └─────────┘└─
txt  ─────────┘└────┘    └─────────┘└─
par  ─────────┘└────┘    └─────────┘└─
pid  ───────────────┘    └────────────
st   ──────────────────────────────┘└─
268            constructor, rw h1, exact h2 }
id                             └┘        └┘
src  ─────────┘└─────────┘└┘└─┘  └──────┘  └──
typ  ─────────┘└─────────┘└┘└─┘└┘└──────┘└┘└──
doc  ─────────┘└─────────┘└┘└─┘  └──────┘  └──
txt  ─────────┘└─────────┘└┘└─┘  └──────┘  └──
par  ─────────┘└─────────┘└┘└─┘  └──────┘  └──
pid  ─────────────────────────┘  └──────┘  └──
st   ────────────────────┘└─────┘└─────────┘└─
269        end
src  ──────────
typ  ──────────
doc  ──────────
txt  ──────────
par  ──────────
pid  ──────────
st   ────────┘
270      end,
src  ──────┘
typ  ──────┘
doc  ──────┘
txt  ──────┘
par  ──────┘
pid  ──────┘
st   ──────┘└─
271      exact ⟨s₁, s₂, rfl, rfl, r⟩
id              └┘  └┘       └─┘  
src      └────┘   └┘  └┘   └┘└─┘└┘ └─
typ      └────┘ └┘└┘└┘└┘   └┘└─┘└┘└─
doc      └────┘   └┘  └┘   └┘   └┘ └─
txt      └────┘   └┘  └┘   └┘   └┘ └─
par      └────┘   └┘  └┘   └┘   └┘ └─
pid              └┘  └┘   └┘   └┘ 
st   ────────────────────────────────
272    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
273  end bisim
274  
275  theorem coinduction : ∀ {s₁ s₂ : seq α}, head s₁ = head s₂ →
id                                   └─┘    └──┘ └┘  └──┘ └┘
src                                   └─┘     └──┘     └──┘
typ                                  └─┘    └──┘ └┘  └──┘ └┘
doc                                   └─┘     └──┘      └──┘
276    (∀ (β : Type u) (fr : seq α → β),
id            └──┘          └─┘   
src                          └─┘
typ           └──┘          └─┘   
doc                          └─┘
277      fr s₁ = fr s₂ → fr (tail s₁) = fr (tail s₂)) → s₁ = s₂
id       └┘ └┘  └┘ └┘   └┘  └──┘ └┘   └┘  └──┘ └┘     └┘  └┘
src                         └──┘          └──┘           
typ      └┘ └┘  └┘ └┘   └┘  └──┘ └┘   └┘  └──┘ └┘     └┘  └┘
doc                          └──┘           └──┘
278  | ⟨f₁, a₁⟩ ⟨f₂, a₂⟩ hh ht :=
id                       └┘ └┘
typ                      └┘ └┘
279    subtype.eq (stream.coinduction hh (λ β fr, ht β (λs, fr s.1)))
id     └────────┘  └────────────────┘        └┘          └┘ 
src    └────────┘  └────────────────┘                           
typ    └────────┘  └────────────────┘        └┘          └┘ 
280  
281  theorem coinduction2 (s) (f g : seq α → seq β)
id                                   └─┘    └─┘ 
src                                  └─┘     └─┘
typ                                  └─┘    └─┘ 
doc                                  └─┘     └─┘
282    (H : ∀ s, bisim_o (λ (s1 s2 : seq β), ∃ (s : seq α), s1 = f s ∧ s2 = g s)
id              └─────┘             └─┘          └─┘   └┘     └┘   
src              └─────┘             └─┘           └─┘                
typ             └─────┘             └─┘          └─┘   └┘     └┘   
doc                                  └─┘            └─┘
283      (destruct (f s)) (destruct (g s)))
id        └──────┘       └──────┘   
src       └──────┘         └──────┘
typ       └──────┘       └──────┘   
doc       └──────┘         └──────┘
284    : f s = g s :=
id           
src          
typ          
285  begin
st   └─────
286    refine eq_of_bisim (λ s1 s2, ∃ s, s1 = f s ∧ s2 = g s) _ ⟨s, rfl, rfl⟩,
id            └─────────┘                                          └─┘
src    └─────┘└─────────┘  └──────┘└┘          └──┘  └┘   └┘└─┘
typ    └─────┘└─────────┘  └──────┘└┘        └──┘ └┘   └┘└─┘
doc    └─────┘             └──────┘ └┘            └──┘  └┘   └┘   
txt    └─────┘             └──────┘ └┘            └──┘  └┘   └┘   
par    └─────┘             └──────┘ └┘            └──┘  └┘   └┘   
pid                       └──────┘ └┘            └──┘  └┘   └┘   
st   ───────────────────────────────────────────────────────────────────────┘└─
287    intros s1 s2 h, rcases h with ⟨s, h1, h2⟩,
id                            
src    └────────────┘  └─────┘ └───────────────┘
typ    └────────────┘  └─────┘└───────────────┘
doc    └────────────┘  └─────┘ └───────────────┘
txt    └────────────┘  └─────┘ └───────────────┘
par    └────────────┘  └─────┘ └───────────────┘
pid          └──────┘         └───────────────┘
st   ───────────────┘└─────────────────────────┘└─
288    rw [h1, h2], apply H
id         └┘  └┘
src    └──┘  └┘    └────┘ 
typ    └──┘└┘└┘└┘  └────┘ 
doc    └──┘  └┘    └────┘ 
txt    └──┘  └┘    └────┘ 
par    └──┘  └┘    └────┘ 
pid      └┘  └┘          
st   ───────┘└──┘└─────────┘
289  end
st   └─┘
290  
291  /-- Embed an infinite stream as a sequence -/
292  def of_stream (s : stream α) : seq α :=
id                      └────┘     └─┘ 
src                     └────┘      └─┘
typ                     └────┘     └─┘ 
doc                                 └─┘
293  ⟨s.map some, λn h, by contradiction⟩
id    └──┘ └──┘    
src    └──┘ └──┘           └───────────┘
typ   └──┘ └──┘         └───────────┘
doc                        └───────────┘
txt                        └───────────┘
par                        └───────────┘
st                        └────────────┘
294  
295  instance coe_stream : has_coe (stream α) (seq α) := ⟨of_stream⟩
id                         └─────┘  └────┘    └─┘       └───────┘
src                        └─────┘  └────┘     └─┘        └───────┘
typ                        └─────┘  └────┘    └─┘       └───────┘
doc                                            └─┘        └───────┘
296  
297  /-- Embed a `lazy_list α` as a sequence. Note that even though this
298    is non-meta, it will produce infinite sequences if used with
299    cyclic `lazy_list`s created by meta constructions. -/
300  def of_lazy_list : lazy_list α → seq α :=
id                      └───────┘    └─┘ 
src                     └───────┘     └─┘
typ                     └───────┘    └─┘ 
doc                                   └─┘
301  corec (λl, match l with
id   └───┘           
src  └───┘
typ  └───┘           
doc  └───┘
302    | lazy_list.nil := none
id       └───────────┘    └──┘
src      └───────────┘    └──┘
typ      └───────────┘    └──┘
303    | lazy_list.cons a l' := some (a, l' ())
id       └────────────┘  └┘    └──┘       └┘
src      └────────────┘         └──┘       └┘
typ      └────────────┘  └┘    └──┘       └┘
304    end)
305  
306  instance coe_lazy_list : has_coe (lazy_list α) (seq α) := ⟨of_lazy_list⟩
id                            └─────┘  └───────┘    └─┘       └──────────┘
src                           └─────┘  └───────┘     └─┘        └──────────┘
typ                           └─────┘  └───────┘    └─┘       └──────────┘
doc                                                  └─┘        └──────────┘
307  
308  /-- Translate a sequence into a `lazy_list`. Since `lazy_list` and `list`
309    are isomorphic as non-meta types, this function is necessarily meta. -/
310  meta def to_lazy_list : seq α → lazy_list α | s :=
id                           └─┘   └───────┘    
src                          └─┘     └───────┘
typ                          └─┘   └───────┘    
doc                          └─┘
311  match destruct s with
id         └──────┘
src        └──────┘
typ        └──────┘
doc        └──────┘
312  | none := lazy_list.nil
id     └──┘    └───────────┘
src    └──┘    └───────────┘
typ    └──┘    └───────────┘
313  | some (a, s') := lazy_list.cons a (to_lazy_list s')
id     └──┘   └┘     └────────────┘    └──────────┘
src    └──┘           └────────────┘
typ    └──┘   └┘     └────────────┘    └──────────┘
314  end
315  
316  /-- Translate a sequence to a list. This function will run forever if
317    run on an infinite sequence. -/
318  meta def force_to_list (s : seq α) : list α := (to_lazy_list s).to_list
id                               └─┘     └──┘      └──────────┘  └─────┘
src                              └─┘      └──┘       └──────────┘   └─────┘
typ                              └─┘     └──┘      └──────────┘  └─────┘
doc                              └─┘                 └──────────┘
319  
320  /-- The sequence of natural numbers some 0, some 1, ... -/
321  def nats : seq ℕ := stream.nats
id              └─┘     └─────────┘
src             └─┘     └─────────┘
typ             └─┘     └─────────┘
doc             └─┘
322  
323  @[simp]
doc    └──┘
324  lemma nats_nth (n : ℕ) : nats.nth n = some n := rfl
id                           └──┘└──┘   └──┘     └─┘
src                          └──┘└──┘    └──┘      └─┘
typ                          └──┘└──┘   └──┘     └─┘
doc                           └──┘└──┘
325  
326  /-- Append two sequences. If `s₁` is infinite, then `s₁ ++ s₂ = s₁`,
327    otherwise it puts `s₂` at the location of the `nil` in `s₁`. -/
328  def append (s₁ s₂ : seq α) : seq α :=
id                       └─┘     └─┘ 
src                      └─┘      └─┘
typ                      └─┘     └─┘ 
doc                      └─┘      └─┘
329  @corec α (seq α × seq α) (λ⟨s₁, s₂⟩,
id    └───┘   └─┘   └─┘     └┘  └┘
src   └───┘    └─┘    └─┘
typ   └───┘   └─┘   └─┘     └┘  └┘
doc   └───┘    └─┘     └─┘
330    match destruct s₁ with
id           └──────┘
src          └──────┘
typ          └──────┘
doc          └──────┘
331    | none := omap (λs₂, (nil, s₂)) (destruct s₂)
id       └──┘    └──┘   └┘  └─┘  └┘    └──────┘
src      └──┘    └──┘       └─┘        └──────┘
typ      └──┘    └──┘   └┘  └─┘  └┘    └──────┘
doc              └──┘        └─┘        └──────┘
332    | some (a, s₁') := some (a, s₁', s₂)
id       └──┘   └─┘     └──┘ 
src      └──┘            └──┘ 
typ      └──┘   └─┘     └──┘ 
333    end) (s₁, s₂)
id          └┘  └┘
src         
typ         └┘  └┘
334  
335  /-- Map a function over a sequence. -/
336  def map (f : α → β) : seq α → seq β | ⟨s, al⟩ :=
id                       └─┘   └─┘     
src                        └─┘     └─┘
typ                      └─┘   └─┘     
doc                        └─┘     └─┘
337  ⟨s.map (option.map f),
id     └──┘  └────────┘ 
src    └──┘  └────────┘
typ    └──┘  └────────┘ 
338  λn, begin
id    
typ   
st       └─────
339    dsimp [stream.map, stream.nth],
id            └────────┘  └────────┘
src    └─────┘└────────┘└┘└────────┘
typ    └─────┘└────────┘└┘└────────┘
doc    └─────┘          └┘          
txt    └─────┘          └┘          
par    └─────┘          └┘          
pid                   └┘          
st   ───────────────────────────────┘└─
340    induction e : s n; intro,
id                    
src    └────────┘ └─┘    └───┘
typ    └────────┘ └─┘  └───┘
doc    └────────┘ └─┘    └───┘
txt    └────────┘ └─┘    └───┘
par    └────────┘ └─┘    └───┘
pid              └─┘ 
st   ─────────────────────────┘└─
341    { rw al e, assumption }, { contradiction }
id          └┘ 
src      └─┘     └─────────┘     └────────────┘
typ      └─┘└┘  └─────────┘     └────────────┘
doc      └─┘     └─────────┘     └────────────┘
txt      └─┘     └─────────┘     └────────────┘
par      └─┘     └─────────┘     └────────────┘
pid                                         
st   ───┘└─────┘└───────────┘└┘└───────────────┘└─
342  end⟩
st   ──┘
343  
344  /-- Flatten a sequence of sequences. (It is required that the
345    sequences be nonempty to ensure productivity; in the case
346    of an infinite sequence of `nil`, the first element is never
347    generated.) -/
348  def join : seq (seq1 α) → seq α :=
id              └─┘  └──┘     └─┘ 
src             └─┘  └──┘      └─┘
typ             └─┘  └──┘     └─┘ 
doc             └─┘  └──┘      └─┘
349  corec (λS, match destruct S with
id   └───┘           └──────┘ 
src  └───┘            └──────┘
typ  └───┘           └──────┘ 
doc  └───┘            └──────┘
350    | none := none
id       └──┘    └──┘
src      └──┘    └──┘
typ      └──┘    └──┘
351    | some ((a, s), S') := some (a, match destruct s with
id       └──┘ └┘     └┘     └──┘          └──────┘
src      └──┘ └┘              └──┘          └──────┘
typ      └──┘ └┘     └┘     └──┘          └──────┘
doc                                          └──────┘
352      | none := S'
id         └──┘
src        └──┘
typ        └──┘
353      | some s' := cons s' S'
id         └──┘ └┘    └──┘
src        └──┘       └──┘
typ        └──┘ └┘    └──┘
doc                   └──┘
354      end)
355    end)
356  
357  /-- Remove the first `n` elements from the sequence. -/
358  def drop (s : seq α) : ℕ → seq α
id                 └─┘       └─┘ 
src                └─┘         └─┘
typ                └─┘       └─┘ 
doc                └─┘          └─┘
359  | 0     := s
id              
typ             
360  | (n+1) := tail (drop n)
id            └──┘  └──┘
src            └──┘
typ           └──┘  └──┘
doc             └──┘
361  attribute [simp] drop
id                    └──┘
src                   └──┘
typ                   └──┘
doc             └──┘  └──┘
362  
363  /-- Take the first `n` elements of the sequence (producing a list) -/
364  def take : ℕ → seq α → list α
id                └─┘    └──┘ 
src                └─┘     └──┘
typ               └─┘    └──┘ 
doc                 └─┘
365  | 0     s := []
id                └┘
src               └┘
typ               └┘
366  | (n+1) s := match destruct s with
id                   └──────┘
src                    └──────┘
typ                  └──────┘
doc                     └──────┘
367    | none := []
id       └──┘    └┘
src      └──┘    └┘
typ      └──┘    └┘
368    | some (x, r) := list.cons x (take n r)
id       └──┘        └───────┘    └──┘
src      └──┘          └───────┘
typ      └──┘        └───────┘    └──┘
369    end
370  
371  /-- Split a sequence at `n`, producing a finite initial segment
372    and an infinite tail. -/
373  def split_at : ℕ → seq α → list α × seq α
id                    └─┘    └──┘   └─┘ 
src                    └─┘     └──┘    └─┘
typ                   └─┘    └──┘   └─┘ 
doc                     └─┘              └─┘
374  | 0     s := ([], s)
id               └┘
src               └┘
typ              └┘
375  | (n+1) s := match destruct s with
id                   └──────┘
src                    └──────┘
typ                  └──────┘
doc                     └──────┘
376    | none := ([], nil)
id       └──┘    └┘  └─┘
src      └──┘    └┘  └─┘
typ      └──┘    └┘  └─┘
doc                   └─┘
377    | some (x, s') := let (l, r) := split_at n s' in (list.cons x l, r)
id       └──┘   └┘     └─┘        └──────┘         └───────┘
src      └──┘                                         └───────┘
typ      └──┘   └┘     └─┘        └──────┘         └───────┘
378    end
379  
380  section zip_with
381  
382  /-- Combine two sequences with a function -/
383  def zip_with (f : α → β → γ) : seq α → seq β → seq γ
id                               └─┘   └─┘    └─┘ 
src                                 └─┘     └─┘     └─┘
typ                              └─┘   └─┘    └─┘ 
doc                                 └─┘     └─┘     └─┘
384  | ⟨f₁, a₁⟩ ⟨f₂, a₂⟩ := ⟨λn,
id      └┘       └┘           
typ     └┘       └┘           
385      match f₁ n, f₂ n with
id                     
typ                    
386      | some a, some b := some (f a b)
id                └──┘     └──┘  
src                └──┘      └──┘
typ               └──┘     └──┘  
387      | _, _ := none
id                 └──┘
src                └──┘
typ                └──┘
388      end,
389    λn, begin
id      
typ     
st         └─────
390      induction h1 : f₁ n,
id                      └┘ 
src      └────────┘  └─┘  
typ      └────────┘  └─┘└┘
doc      └────────┘  └─┘  
txt      └────────┘  └─┘  
par      └────────┘  └─┘  
pid                 └─┘  
st   ──────────────────────┘└─
391      { intro H, simp only [(a₁ h1)], refl },
id                              └┘ └┘
src        └─────┘  └─────────┘     └┘  └───┘
typ        └─────┘  └─────────┘ └┘└┘└┘  └───┘
doc        └─────┘  └─────────┘     └┘  └───┘
txt        └─────┘  └─────────┘     └┘  └───┘
par        └─────┘  └─────────┘     └┘  └───┘
pid             └┘      └──┘└┘     └┘      
st   ─────┘└─────┘└───────────────────┘└─────┘└┘
392      induction h2 : f₂ n; dsimp [seq.zip_with._match_1]; intro H,
id                      └┘          └───────────────────┘
src      └────────┘  └─┘     └─────┘                       └─────┘
typ      └────────┘  └─┘└┘  └─────┘└───────────────────┘  └─────┘
doc      └────────┘  └─┘     └─────┘                       └─────┘
txt      └────────┘  └─┘     └─────┘                       └─────┘
par      └────────┘  └─┘     └─────┘                       └─────┘
pid                 └─┘                                      └┘
st   ──────────────────────────────────────────────────────────────┘└─
393      { rw (a₂ h2), cases f₁ (n + 1); refl },
id             └┘ └┘         └┘   
src        └─┘       └────┘    └─┘  └───┘
typ        └─┘ └┘└┘  └────┘└┘ └─┘  └───┘
doc        └─┘       └────┘     └─┘  └───┘
txt        └─┘       └────┘     └─┘  └───┘
par        └─┘       └────┘     └─┘  └───┘
pid                           └─┘      
st   ─────┘└────────┘└───────────────────────┘└┘
394      { rw [h1, h2] at H, contradiction }
id             └┘  └┘
src        └──┘  └┘  └────┘  └────────────┘
typ        └──┘└┘└┘└┘└────┘  └────────────┘
doc        └──┘  └┘  └────┘  └────────────┘
txt        └──┘  └┘  └────┘  └────────────┘
par        └──┘  └┘  └────┘  └────────────┘
pid          └┘  └┘  └───┘               
st   ───────────┘└──┘└───┘└──────────────┘└─
395    end⟩
st   ────┘
396  
397  variables {s : seq α} {s' : seq β} {n : ℕ}
id                  └─┘          └─┘         
src                 └─┘          └─┘         
typ                 └─┘          └─┘         
doc                 └─┘          └─┘
398  
399  lemma zip_with_nth_some {a : α} {b : β} (s_nth_eq_some : s.nth n = some a)
id                                                          └──┘   └──┘ 
src                                                            └──┘    └──┘
typ                                                         └──┘   └──┘ 
doc                                                            └──┘
400  (s_nth_eq_some' : s'.nth n = some b) (f : α → β → γ) :
id                     └┘└──┘   └──┘              
src                      └──┘    └──┘
typ                    └┘└──┘   └──┘              
doc                      └──┘
401    (zip_with f s s').nth n = some (f a b) :=
id      └──────┘   └┘ └─┘    └──┘    
src     └──────┘        └─┘     └──┘
typ     └──────┘   └┘ └─┘    └──┘    
doc     └──────┘        └─┘
402  begin
st   └─────
403    cases s with st,
id           
src    └────┘ └──────┘
typ    └────┘└──────┘
doc    └────┘ └──────┘
txt    └────┘ └──────┘
par    └────┘ └──────┘
pid          └──────┘
st   ────────────────┘└─
404    have : st n = some a, from s_nth_eq_some,
id            └┘   └──┘        └───────────┘
src    └─────┘   └──┘   └───┘
typ    └─────┘└┘└──┘  └───┘└───────────┘
doc    └─────┘           └───┘
txt    └─────┘           └───┘
par    └─────┘           └───┘
pid    └───┘└┘           └───┘
st   ─────────────────────┘└──────────────────┘└─
405    cases s' with st',
id           └┘
src    └────┘  └───────┘
typ    └────┘└┘└───────┘
doc    └────┘  └───────┘
txt    └────┘  └───────┘
par    └────┘  └───────┘
pid           └───────┘
st   ──────────────────┘└─
406    have : st' n = some b, from s_nth_eq_some',
id            └─┘    └──┘        └────────────┘
src    └─────┘     └──┘   └───┘
typ    └─────┘└─┘ └──┘  └───┘└────────────┘
doc    └─────┘            └───┘
txt    └─────┘            └───┘
par    └─────┘            └───┘
pid    └───┘└┘            └───┘
st   ──────────────────────┘└───────────────────┘└─
407    simp only [zip_with, seq.nth, *]
id                └──────┘  └─────┘
src    └─────────┘└──────┘└┘└─────┘└───┘
typ    └─────────┘└──────┘└┘└─────┘└───┘
doc    └─────────┘└──────┘└┘└─────┘└───┘
txt    └─────────┘        └┘       └───┘
par    └─────────┘        └┘       └───┘
pid        └──┘└┘        └┘       └──┘
st   ──────────────────────────────────┘
408  end
st   └─┘
409  
410  lemma zip_with_nth_none (s_nth_eq_none : s.nth n = none) (f : α → β → γ) :
id                                            └──┘   └──┘             
src                                            └──┘    └──┘
typ                                           └──┘   └──┘             
doc                                            └──┘
411    (zip_with f s s').nth n = none :=
id      └──────┘   └┘ └─┘    └──┘
src     └──────┘        └─┘     └──┘
typ     └──────┘   └┘ └─┘    └──┘
doc     └──────┘        └─┘
412  begin
st   └─────
413    cases s with st,
id           
src    └────┘ └──────┘
typ    └────┘└──────┘
doc    └────┘ └──────┘
txt    └────┘ └──────┘
par    └────┘ └──────┘
pid          └──────┘
st   ────────────────┘└─
414    have : st n = none, from s_nth_eq_none,
id            └┘   └──┘       └───────────┘
src    └─────┘   └──┘  └───┘
typ    └─────┘└┘└──┘  └───┘└───────────┘
doc    └─────┘          └───┘
txt    └─────┘          └───┘
par    └─────┘          └───┘
pid    └───┘└┘          └───┘
st   ───────────────────┘└──────────────────┘└─
415    cases s' with st',
id           └┘
src    └────┘  └───────┘
typ    └────┘└┘└───────┘
doc    └────┘  └───────┘
txt    └────┘  └───────┘
par    └────┘  └───────┘
pid           └───────┘
st   ──────────────────┘└─
416    cases st'_nth_eq : st' n;
id                        └─┘ 
src    └────┘          └─┘   
typ    └────┘          └─┘└─┘
doc    └────┘          └─┘   
txt    └────┘          └─┘   
par    └────┘          └─┘   
pid                   └─┘   
st   ────────────────────────────
417    simp only [zip_with, seq.nth, *]
id                └──────┘  └─────┘
src    └─────────┘└──────┘└┘└─────┘└───┘
typ    └─────────┘└──────┘└┘└─────┘└───┘
doc    └─────────┘└──────┘└┘└─────┘└───┘
txt    └─────────┘        └┘       └───┘
par    └─────────┘        └┘       └───┘
pid        └──┘└┘        └┘       └──┘
st   ──────────────────────────────────┘
418  end
st   └─┘
419  
420  lemma zip_with_nth_none' (s'_nth_eq_none : s'.nth n = none) (f : α → β → γ) :
id                                              └┘└──┘   └──┘             
src                                               └──┘    └──┘
typ                                             └┘└──┘   └──┘             
doc                                               └──┘
421    (zip_with f s s').nth n = none :=
id      └──────┘   └┘ └─┘    └──┘
src     └──────┘        └─┘     └──┘
typ     └──────┘   └┘ └─┘    └──┘
doc     └──────┘        └─┘
422  begin
st   └─────
423    cases s' with st',
id           └┘
src    └────┘  └───────┘
typ    └────┘└┘└───────┘
doc    └────┘  └───────┘
txt    └────┘  └───────┘
par    └────┘  └───────┘
pid           └───────┘
st   ──────────────────┘└─
424    have : st' n = none, from s'_nth_eq_none,
id            └─┘   └──┘       └────────────┘
src    └─────┘    └──┘  └───┘
typ    └─────┘└─┘└──┘  └───┘└────────────┘
doc    └─────┘           └───┘
txt    └─────┘           └───┘
par    └─────┘           └───┘
pid    └───┘└┘           └───┘
st   ────────────────────┘└───────────────────┘└─
425    cases s with st,
id           
src    └────┘ └──────┘
typ    └────┘└──────┘
doc    └────┘ └──────┘
txt    └────┘ └──────┘
par    └────┘ └──────┘
pid          └──────┘
st   ────────────────┘└─
426    cases st_nth_eq : st n;
id                       └┘ 
src    └────┘         └─┘  
typ    └────┘         └─┘└┘
doc    └────┘         └─┘  
txt    └────┘         └─┘  
par    └────┘         └─┘  
pid                  └─┘  
st   ──────────────────────────
427    simp only [zip_with, seq.nth, *]
id                └──────┘  └─────┘
src    └─────────┘└──────┘└┘└─────┘└───┘
typ    └─────────┘└──────┘└┘└─────┘└───┘
doc    └─────────┘└──────┘└┘└─────┘└───┘
txt    └─────────┘        └┘       └───┘
par    └─────────┘        └┘       └───┘
pid        └──┘└┘        └┘       └──┘
st   ──────────────────────────────────┘
428  end
st   └─┘
429  
430  end zip_with
431  
432  /-- Pair two sequences into a sequence of pairs -/
433  def zip : seq α → seq β → seq (α × β) := zip_with prod.mk
id             └─┘    └─┘    └─┘         └──────┘ └─────┘
src            └─┘     └─┘     └─┘           └──────┘ └─────┘
typ            └─┘    └─┘    └─┘         └──────┘ └─────┘
doc            └─┘     └─┘     └─┘            └──────┘
434  
435  /-- Separate a sequence of pairs into two sequences -/
436  def unzip (s : seq (α × β)) : seq α × seq β := (map prod.fst s, map prod.snd s)
id                  └─┘         └─┘   └─┘     └─┘ └──────┘   └─┘ └──────┘ 
src                 └─┘           └─┘    └─┘      └─┘ └──────┘    └─┘ └──────┘
typ                 └─┘         └─┘   └─┘     └─┘ └──────┘   └─┘ └──────┘ 
doc                 └─┘            └─┘     └─┘       └─┘             └─┘
437  
438  /-- Convert a sequence which is known to terminate into a list -/
439  def to_list (s : seq α) (h : ∃ n, ¬ (nth s n).is_some) : list α :=
id                    └─┘            └─┘   └─────┘     └──┘ 
src                   └─┘              └─┘     └─────┘     └──┘
typ                   └─┘            └─┘   └─────┘     └──┘ 
doc                   └─┘                 └─┘
440  take (nat.find h) s
id   └──┘  └──────┘   
src  └──┘  └──────┘
typ  └──┘  └──────┘   
doc  └──┘
441  
442  /-- Convert a sequence which is known not to terminate into a stream -/
443  def to_stream (s : seq α) (h : ∀ n, (nth s n).is_some) : stream α :=
id                      └─┘             └─┘   └─────┘     └────┘ 
src                     └─┘               └─┘     └─────┘     └────┘
typ                     └─┘             └─┘   └─────┘     └────┘ 
doc                     └─┘               └─┘
444  λn, option.get (h n)
id      └────────┘   
src      └────────┘
typ     └────────┘   
445  
446  /-- Convert a sequence into either a list or a stream depending on whether
447    it is finite or infinite. (Without decidability of the infiniteness predicate,
448    this is not constructively possible.) -/
449  def to_list_or_stream (s : seq α) [decidable (∃ n, ¬ (nth s n).is_some)] :
id                              └─┘    └───────┘      └─┘   └─────┘
src                             └─┘     └───────┘       └─┘     └─────┘
typ                             └─┘    └───────┘      └─┘   └─────┘
doc                             └─┘                        └─┘
450    list α ⊕ stream α :=
id     └──┘   └────┘ 
src    └──┘    └────┘
typ    └──┘   └────┘ 
451  if h : ∃ n, ¬ (nth s n).is_some
id   └┘         └─┘   └─────┘
src  └┘          └─┘     └─────┘
typ  └┘         └─┘   └─────┘
doc                 └─┘
452  then sum.inl (to_list s h)
id        └─────┘  └─────┘  
src       └─────┘  └─────┘
typ       └─────┘  └─────┘  
doc                └─────┘
453  else sum.inr (to_stream s (λn, decidable.by_contradiction (λ hn, h ⟨n, hn⟩)))
id        └─────┘  └───────┘      └────────────────────────┘    └┘      └┘
src       └─────┘  └───────┘        └────────────────────────┘
typ       └─────┘  └───────┘      └────────────────────────┘    └┘      └┘
doc                └───────┘
454  
455  @[simp] theorem nil_append (s : seq α) : append nil s = s :=
id                                   └─┘     └────┘ └─┘   
src                                  └─┘      └────┘ └─┘   
typ                                  └─┘     └────┘ └─┘   
doc    └──┘                          └─┘      └────┘ └─┘
456  begin
st   └─────
457    apply coinduction2, intro s,
id           └──────────┘
src    └────┘└──────────┘  └─────┘
typ    └────┘└──────────┘  └─────┘
doc    └────┘              └─────┘
txt    └────┘              └─────┘
par    └────┘              └─────┘
pid                            └┘
st   ───────────────────┘└───────┘└─
458    dsimp [append], rw [corec_eq],
id            └────┘       └──────┘
src    └─────┘└────┘  └──┘└──────┘
typ    └─────┘└────┘  └──┘└──────┘
doc    └─────┘└────┘  └──┘        
txt    └─────┘        └──┘        
par    └─────┘        └──┘        
pid                   └┘        
st   ───────────────┘└────────────┘└──
459    dsimp [append], apply cases_on s _ _,
id            └────┘         └──────┘ 
src    └─────┘└────┘  └────┘└──────┘ └──┘
typ    └─────┘└────┘  └────┘└──────┘└──┘
doc    └─────┘└────┘  └────┘         └──┘
txt    └─────┘        └────┘         └──┘
par    └─────┘        └────┘         └──┘
pid                               └──┘
st   ───────────────┘└────────────────────┘└─
460    { trivial },
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid             
st   ───┘└──────┘└┘
461    { intros x s,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid            └──┘
st   ─────────────┘└─
462      rw [destruct_cons], dsimp,
id           └───────────┘
src      └──┘└───────────┘  └───┘
typ      └──┘└───────────┘  └───┘
doc      └──┘               └───┘
txt      └──┘               └───┘
par      └──┘               └───┘
pid        └┘             
st   ────────────────────┘└──────┘└─
463      exact ⟨rfl, s, rfl, rfl⟩ }
id                          └─┘
src      └────┘    └┘ └┘   └┘└─┘└┘
typ      └────┘    └┘└┘   └┘└─┘└┘
doc      └────┘    └┘ └┘   └┘   └┘
txt      └────┘    └┘ └┘   └┘   └┘
par      └────┘    └┘ └┘   └┘   └┘
pid               └┘ └┘   └┘   
st   ────────────────────────────┘└─
464  end
st   ──┘
465  
466  @[simp] theorem cons_append (a : α) (s t) : append (cons a s) t = cons a (append s t) :=
id                                              └────┘  └──┘      └──┘   └────┘  
src                                              └────┘  └──┘         └──┘    └────┘
typ                                             └────┘  └──┘      └──┘   └────┘  
doc    └──┘                                      └────┘  └──┘          └──┘    └────┘
467  destruct_eq_cons $ begin
id   └──────────────┘
src  └──────────────┘
typ  └──────────────┘
st                      └─────
468    dsimp [append], rw [corec_eq],
id            └────┘       └──────┘
src    └─────┘└────┘  └──┘└──────┘
typ    └─────┘└────┘  └──┘└──────┘
doc    └─────┘└────┘  └──┘        
txt    └─────┘        └──┘        
par    └─────┘        └──┘        
pid                   └┘        
st   ───────────────┘└────────────┘└──
469    dsimp [append], rw [destruct_cons],
id            └────┘       └───────────┘
src    └─────┘└────┘  └──┘└───────────┘
typ    └─────┘└────┘  └──┘└───────────┘
doc    └─────┘└────┘  └──┘             
txt    └─────┘        └──┘             
par    └─────┘        └──┘             
pid                   └┘             
st   ───────────────┘└─────────────────┘└──
470    dsimp [append], refl
id            └────┘
src    └─────┘└────┘  └───┘
typ    └─────┘└────┘  └───┘
doc    └─────┘└────┘  └───┘
txt    └─────┘        └───┘
par    └─────┘        └───┘
pid                     
st   ───────────────┘└─────┘
471  end
st   └─┘
472  
473  @[simp] theorem append_nil (s : seq α) : append s nil = s :=
id                                   └─┘     └────┘  └─┘  
src                                  └─┘      └────┘   └─┘ 
typ                                  └─┘     └────┘  └─┘  
doc    └──┘                          └─┘      └────┘   └─┘
474  begin
st   └─────
475    apply coinduction2 s, intro s,
id           └──────────┘ 
src    └────┘└──────────┘   └─────┘
typ    └────┘└──────────┘  └─────┘
doc    └────┘               └─────┘
txt    └────┘               └─────┘
par    └────┘               └─────┘
pid                             └┘
st   ─────────────────────┘└───────┘└─
476    apply cases_on s _ _,
id           └──────┘ 
src    └────┘└──────┘ └──┘
typ    └────┘└──────┘└──┘
doc    └────┘         └──┘
txt    └────┘         └──┘
par    └────┘         └──┘
pid                  └──┘
st   ─────────────────────┘└─
477    { trivial },
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid             
st   ───┘└──────┘└┘
478    { intros x s,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid            └──┘
st   ─────────────┘└─
479      rw [cons_append, destruct_cons, destruct_cons], dsimp,
id           └─────────┘  └───────────┘  └───────────┘
src      └──┘└─────────┘└┘└───────────┘└┘└───────────┘  └───┘
typ      └──┘└─────────┘└┘└───────────┘└┘└───────────┘  └───┘
doc      └──┘           └┘             └┘               └───┘
txt      └──┘           └┘             └┘               └───┘
par      └──┘           └┘             └┘               └───┘
pid        └┘           └┘             └┘             
st   ──────────────────┘└─────────────┘└─────────────┘└──────┘└─
480      exact ⟨rfl, s, rfl, rfl⟩ }
id                          └─┘
src      └────┘    └┘ └┘   └┘└─┘└┘
typ      └────┘    └┘└┘   └┘└─┘└┘
doc      └────┘    └┘ └┘   └┘   └┘
txt      └────┘    └┘ └┘   └┘   └┘
par      └────┘    └┘ └┘   └┘   └┘
pid               └┘ └┘   └┘   
st   ────────────────────────────┘└─
481  end
st   ──┘
482  
483  @[simp] theorem append_assoc (s t u : seq α) :
id                                         └─┘ 
src                                        └─┘
typ                                        └─┘ 
doc    └──┘                                └─┘
484    append (append s t) u = append s (append t u) :=
id     └────┘  └────┘      └────┘   └────┘  
src    └────┘  └────┘         └────┘    └────┘
typ    └────┘  └────┘      └────┘   └────┘  
doc    └────┘  └────┘          └────┘    └────┘
485  begin
st   └─────
486    apply eq_of_bisim (λs1 s2, ∃ s t u,
id           └─────────┘                
src    └────┘└─────────┘  └─────┘└────┘
typ    └────┘└─────────┘  └─────┘└────┘
doc    └────┘             └─────┘ └────┘ 
txt    └────┘             └─────┘ └────┘ 
par    └────┘             └─────┘ └────┘ 
pid                      └─────┘ └────┘ 
st   ──────────────────────────────────────
487      s1 = append (append s t) u ∧ s2 = append s (append t u)),
id                                                 └────┘
src  ───┘                 └┘            └────┘  └┘
typ  ───┘                 └┘            └────┘  └┘
doc  ───┘                  └┘             └────┘  └┘
txt  ───┘                  └┘                     └┘
par  ───┘                  └┘                     └┘
pid  ───┘                  └┘                     └┘
st   ───────────────────────────────────────────────────────────┘└─
488    { intros s1 s2 h, exact match s1, s2, h with ._, ._, ⟨s, t, u, rfl, rfl⟩ := begin
id                                   └┘  └┘                               └─┘
src      └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘ └┘   └┘└─┘└───┘     
typ      └────────────┘  └────┘     └┘└┘└┘└┘└────┘  └┘  └┘  └┘ └┘ └┘   └┘└─┘└───┘     
doc      └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘ └┘   └┘   └───┘     
txt      └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘ └┘   └┘   └───┘     
par      └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘ └┘   └┘   └───┘     
pid            └──────┘              └┘  └┘ └────┘  └┘  └┘  └┘ └┘ └┘   └┘   └───┘     
st   ───┘└────────────┘└──────────────────────────────────────────────────────────┘└─────
489        apply cases_on s; simp,
id               └──────┘ 
src  ─────┘└────┘└──────┘ └┘└──┘└─
typ  ───────────┘└──────┘└┘└──┘└─
doc  ─────┘└────┘         └┘└──┘└─
txt  ─────┘└────┘         └┘└──┘└─
par  ───────────┘         └┘└──┘└─
pid  ───────────┘         └───────
st   ───────────────────────────┘└─
490        { apply cases_on t; simp,
id                 └──────┘ 
src  ───────┘└────┘└──────┘ └┘└──┘└─
typ  ─────────────┘└──────┘└┘└──┘└─
doc  ───────┘└────┘         └┘└──┘└─
txt  ───────┘└────┘         └┘└──┘└─
par  ─────────────┘         └┘└──┘└─
pid  ─────────────┘         └───────
st   ──────┘└─────────────────────┘└─
491          { apply cases_on u; simp,
id                   └──────┘ 
src  ─────────┘└────┘└──────┘ └┘└──┘└─
typ  ───────────────┘└──────┘└┘└──┘└─
doc  ─────────┘└────┘         └┘└──┘└─
txt  ─────────┘└────┘         └┘└──┘└─
par  ───────────────┘         └┘└──┘└─
pid  ───────────────┘         └───────
st   ────────┘└─────────────────────┘└─
492            { intros x u, refine ⟨nil, nil, u, _, _⟩; simp } },
id                                        └─┘  
src  ───────────┘└────────┘└┘└─────┘    └┘└─┘└┘ └─────┘└┘└───┘└────
typ  ───────────┘└────────┘└───────┘    └┘└─┘└┘└───────┘└───┘└────
doc  ───────────┘└────────┘└┘└─────┘    └┘└─┘└┘ └─────┘└┘└───┘└────
txt  ───────────┘└────────┘└┘└─────┘    └┘   └┘ └─────┘└┘└───┘└────
par  ───────────┘└────────┘└───────┘    └┘   └┘ └───────┘└───┘└────
pid  ──────────────────────────────┘    └┘   └┘ └──────────────────
st   ─────────────────────┘└─────────────────────────────────┘└─┘└─
493          { intros x t, refine ⟨nil, t, u, _, _⟩; simp } },
id                                 └─┘    
src  ─────────┘└────────┘└┘└─────┘ └─┘└┘ └┘ └─────┘└┘└───┘└────
typ  ─────────┘└────────┘└───────┘ └─┘└┘└┘└───────┘└───┘└────
doc  ─────────┘└────────┘└┘└─────┘ └─┘└┘ └┘ └─────┘└┘└───┘└────
txt  ─────────┘└────────┘└┘└─────┘    └┘ └┘ └─────┘└┘└───┘└────
par  ─────────┘└────────┘└───────┘    └┘ └┘ └───────┘└───┘└────
pid  ────────────────────────────┘    └┘ └┘ └──────────────────
st   ───────────────────┘└───────────────────────────────┘└─┘└─
494        { intros x s, exact ⟨s, t, u, rfl, rfl⟩ }
id                                         └─┘
src  ───────┘└────────┘└──────┘  └┘ └┘ └┘   └┘└─┘└───
typ  ───────┘└────────┘└──────┘ └┘└┘└┘   └┘└─┘└───
doc  ───────┘└────────┘└──────┘  └┘ └┘ └┘   └┘   └───
txt  ───────┘└────────┘└──────┘  └┘ └┘ └┘   └┘   └───
par  ───────┘└────────┘└──────┘  └┘ └┘ └┘   └┘   └───
pid  ─────────────────────────┘  └┘ └┘ └┘   └┘   └───
st   ─────────────────┘└──────────────────────────┘└─
495      end end },
src  ───────────┘
typ  ───────────┘
doc  ───────────┘
txt  ───────────┘
par  ───────────┘
pid  ──────────┘
st   ──────┘└───┘└┘
496    { exact ⟨s, t, u, rfl, rfl⟩ }
id                         └─┘
src      └────┘  └┘ └┘ └┘   └┘└─┘└┘
typ      └────┘ └┘└┘└┘   └┘└─┘└┘
doc      └────┘  └┘ └┘ └┘   └┘   └┘
txt      └────┘  └┘ └┘ └┘   └┘   └┘
par      └────┘  └┘ └┘ └┘   └┘   └┘
pid             └┘ └┘ └┘   └┘   
st   ─────────────────────────────┘└─
497  end
st   ──┘
498  
499  @[simp] theorem map_nil (f : α → β) : map f nil = nil := rfl
id                                       └─┘  └─┘  └─┘    └─┘
src                                        └─┘   └─┘  └─┘    └─┘
typ                                      └─┘  └─┘  └─┘    └─┘
doc    └──┘                                └─┘   └─┘   └─┘
500  
501  @[simp] theorem map_cons (f : α → β) (a) : ∀ s, map f (cons a s) = cons (f a) (map f s)
id                                                └─┘   └──┘     └──┘      └─┘  
src                                                  └─┘    └──┘       └──┘        └─┘
typ                                               └─┘   └──┘     └──┘      └─┘  
doc    └──┘                                          └─┘    └──┘        └──┘        └─┘
502  | ⟨s, al⟩ := by apply subtype.eq; dsimp [cons, map]; rw stream.map_cons; refl
id                         └────────┘         └──┘  └─┘      └─────────────┘
src                  └────┘└────────┘  └─────┘└──┘└┘└─┘  └─┘└─────────────┘  └────
typ                  └────┘└────────┘  └─────┘└──┘└┘└─┘  └─┘└─────────────┘  └────
doc                  └────┘            └─────┘└──┘└┘└─┘  └─┘                 └────
txt                  └────┘            └─────┘    └┘     └─┘                 └────
par                  └────┘            └─────┘    └┘     └─┘                 └────
pid                                            └┘                            
st                  └───────────────────────────────────────┘└─────────────┘└──────
503  
src  
typ  
doc  
txt  
par  
pid  
st   
504  @[simp] theorem map_id : ∀ (s : seq α), map id s = s
id                                  └─┘    └─┘ └┘   
src                                  └─┘     └─┘ └┘   
typ                                 └─┘    └─┘ └┘   
doc    └──┘                          └─┘     └─┘
505  | ⟨s, al⟩ := begin
st                └─────
506    apply subtype.eq; dsimp [map],
id           └────────┘         └─┘
src    └────┘└────────┘  └─────┘└─┘
typ    └────┘└────────┘  └─────┘└─┘
doc    └────┘            └─────┘└─┘
txt    └────┘            └─────┘   
par    └────┘            └─────┘   
pid                             
st   ──────────────────────────────┘└─
507    rw [option.map_id, stream.map_id]; refl
id         └───────────┘  └───────────┘
src    └──┘└───────────┘└┘└───────────┘  └───┘
typ    └──┘└───────────┘└┘└───────────┘  └───┘
doc    └──┘             └┘               └───┘
txt    └──┘             └┘               └───┘
par    └──┘             └┘               └───┘
pid      └┘             └┘                   
st   ──────────────────┘└─────────────┘└─────┘
508  end
st   └─┘
509  
510  @[simp] theorem map_tail (f : α → β) : ∀ s, map f (tail s) = tail (map f s)
id                                            └─┘   └──┘    └──┘  └─┘  
src                                              └─┘    └──┘     └──┘  └─┘
typ                                           └─┘   └──┘    └──┘  └─┘  
doc    └──┘                                      └─┘    └──┘      └──┘  └─┘
511  | ⟨s, al⟩ := by apply subtype.eq; dsimp [tail, map]; rw stream.map_tail; refl
id                         └────────┘         └──┘  └─┘      └─────────────┘
src                  └────┘└────────┘  └─────┘└──┘└┘└─┘  └─┘└─────────────┘  └────
typ                  └────┘└────────┘  └─────┘└──┘└┘└─┘  └─┘└─────────────┘  └────
doc                  └────┘            └─────┘└──┘└┘└─┘  └─┘                 └────
txt                  └────┘            └─────┘    └┘     └─┘                 └────
par                  └────┘            └─────┘    └┘     └─┘                 └────
pid                                            └┘                            
st                  └───────────────────────────────────────┘└─────────────┘└──────
512  
src  
typ  
doc  
txt  
par  
pid  
st   
513  theorem map_comp (f : α → β) (g : β → γ) : ∀ (s : seq α), map (g ∘ f) s = map g (map f s)
id                                                └─┘    └─┘        └─┘   └─┘  
src                                                    └─┘     └─┘           └─┘    └─┘
typ                                               └─┘    └─┘        └─┘   └─┘  
doc                                                    └─┘     └─┘             └─┘    └─┘
514  | ⟨s, al⟩ := begin
st                └─────
515    apply subtype.eq; dsimp [map],
id           └────────┘         └─┘
src    └────┘└────────┘  └─────┘└─┘
typ    └────┘└────────┘  └─────┘└─┘
doc    └────┘            └─────┘└─┘
txt    └────┘            └─────┘   
par    └────┘            └─────┘   
pid                             
st   ──────────────────────────────┘└─
516    rw stream.map_map,
id        └────────────┘
src    └─┘└────────────┘
typ    └─┘└────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ──────────────────┘└─
517    apply congr_arg (λ f : _ → option γ, stream.map f s),
id           └───────┘           └────┘   └────────┘   
src    └────┘└───────┘  └─────┘ └────┘ └┘└────────┘  
typ    └────┘└───────┘  └─────┘└────┘└┘└────────┘ 
doc    └────┘           └─────┘        └┘            
txt    └────┘           └─────┘        └┘            
par    └────┘           └─────┘        └┘            
pid                    └─────┘        └┘            
st   ─────────────────────────────────────────────────────┘└─
518    funext x, cases x with x; refl
id                     
src    └──────┘  └────┘ └─────┘  └───┘
typ    └──────┘  └────┘└─────┘  └───┘
doc    └──────┘  └────┘ └─────┘  └───┘
txt    └──────┘  └────┘ └─────┘  └───┘
par    └──────┘  └────┘ └─────┘  └───┘
pid          └┘        └─────┘      
st   ─────────┘└─────────────────────┘
519  end
st   └─┘
520  
521  @[simp] theorem map_append (f : α → β) (s t) : map f (append s t) = append (map f s) (map f t) :=
id                                                └─┘   └────┘     └────┘  └─┘     └─┘  
src                                                 └─┘    └────┘       └────┘  └─┘       └─┘
typ                                               └─┘   └────┘     └────┘  └─┘     └─┘  
doc    └──┘                                         └─┘    └────┘        └────┘  └─┘       └─┘
522  begin
st   └─────
523    apply eq_of_bisim (λs1 s2, ∃ s t,
id           └─────────┘              
src    └────┘└─────────┘  └─────┘└──┘
typ    └────┘└─────────┘  └─────┘└──┘
doc    └────┘             └─────┘ └──┘ 
txt    └────┘             └─────┘ └──┘ 
par    └────┘             └─────┘ └──┘ 
pid                      └─────┘ └──┘ 
st   ────────────────────────────────────
524      s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)) _ ⟨s, t, rfl, rfl⟩,
id                                    └────┘            └─┘                  └─┘
src  ───┘               └┘   └────┘      └┘ └─┘  └───┘  └┘ └┘   └┘└─┘
typ  ───┘               └┘   └────┘      └┘ └─┘ └───┘ └┘└┘   └┘└─┘
doc  ───┘                └┘    └────┘      └┘ └─┘  └───┘  └┘ └┘   └┘   
txt  ───┘                └┘                └┘      └───┘  └┘ └┘   └┘   
par  ───┘                └┘                └┘      └───┘  └┘ └┘   └┘   
pid  ───┘                └┘                └┘      └───┘  └┘ └┘   └┘   
st   ────────────────────────────────────────────────────────────────────────────────┘└─
525    intros s1 s2 h, exact match s1, s2, h with ._, ._, ⟨s, t, rfl, rfl⟩ := begin
id                                 └┘  └┘  
src    └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘   └┘   └───┘     
typ    └────────────┘  └────┘     └┘└┘└┘└┘└────┘  └┘  └┘  └┘ └┘   └┘   └───┘     
doc    └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘   └┘   └───┘     
txt    └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘   └┘   └───┘     
par    └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘   └┘   └───┘     
pid          └──────┘              └┘  └┘ └────┘  └┘  └┘  └┘ └┘   └┘   └───┘     
st   ───────────────┘└───────────────────────────────────────────────────────┘└─────
526      apply cases_on s; simp,
id             └──────┘ 
src  ───┘└────┘└──────┘ └┘└──┘└─
typ  ─────────┘└──────┘└┘└──┘└─
doc  ───┘└────┘         └┘└──┘└─
txt  ───┘└────┘         └┘└──┘└─
par  ─────────┘         └┘└──┘└─
pid  ─────────┘         └───────
st   ─────────────────────────┘└─
527      { apply cases_on t; simp,
id               └──────┘ 
src  ─────┘└────┘└──────┘ └┘└──┘└─
typ  ───────────┘└──────┘└┘└──┘└─
doc  ─────┘└────┘         └┘└──┘└─
txt  ─────┘└────┘         └┘└──┘└─
par  ───────────┘         └┘└──┘└─
pid  ───────────┘         └───────
st   ────┘└─────────────────────┘└─
528        { intros x t, refine ⟨nil, t, _, _⟩; simp } },
id                               └─┘  
src  ───────┘└────────┘└┘└─────┘ └─┘└┘ └─────┘└┘└───┘└────
typ  ───────┘└────────┘└───────┘ └─┘└┘└───────┘└───┘└────
doc  ───────┘└────────┘└┘└─────┘ └─┘└┘ └─────┘└┘└───┘└────
txt  ───────┘└────────┘└┘└─────┘    └┘ └─────┘└┘└───┘└────
par  ───────┘└────────┘└───────┘    └┘ └───────┘└───┘└────
pid  ──────────────────────────┘    └┘ └──────────────────
st   ─────────────────┘└────────────────────────────┘└─┘└─
529      { intros x s, refine ⟨s, t, rfl, rfl⟩ }
id                                      └─┘
src  ─────┘└────────┘└┘└─────┘  └┘ └┘   └┘└─┘└┘└─
typ  ─────┘└────────┘└───────┘ └┘└┘   └┘└─┘└───
doc  ─────┘└────────┘└┘└─────┘  └┘ └┘   └┘   └┘└─
txt  ─────┘└────────┘└┘└─────┘  └┘ └┘   └┘   └┘└─
par  ─────┘└────────┘└───────┘  └┘ └┘   └┘   └───
pid  ────────────────────────┘  └┘ └┘   └┘   └───
st   ───────────────┘└────────────────────────┘└─
530    end end
src  ─────────┘
typ  ─────────┘
doc  ─────────┘
txt  ─────────┘
par  ─────────┘
pid  ────────┘
st   ────┘└───┘
531  end
st   └─┘
532  
533  @[simp] theorem map_nth (f : α → β) : ∀ s n, nth (map f s) n = (nth s n).map f
id                                            └─┘  └─┘       └─┘   └─┘  
src                                               └─┘  └─┘          └─┘     └─┘
typ                                           └─┘  └─┘       └─┘   └─┘  
doc    └──┘                                       └─┘  └─┘           └─┘
534  | ⟨s, al⟩ n := rfl
id                  └─┘
src                 └─┘
typ                 └─┘
535  
536  instance : functor seq := {map := @map}
id              └─────┘ └─┘             └─┘
src             └─────┘ └─┘             └─┘
typ             └─────┘ └─┘             └─┘
doc                     └─┘             └─┘
537  
538  instance : is_lawful_functor seq :=
id              └───────────────┘ └─┘
src             └───────────────┘ └─┘
typ             └───────────────┘ └─┘
doc                               └─┘
539  { id_map := @map_id, comp_map := @map_comp }
id               └────┘               └──────┘
src              └────┘               └──────┘
typ              └────┘               └──────┘
540  
541  @[simp] theorem join_nil : join nil = (nil : seq α) := destruct_eq_nil rfl
id                              └──┘ └─┘   └─┘   └─┘      └─────────────┘ └─┘
src                             └──┘ └─┘   └─┘   └─┘       └─────────────┘ └─┘
typ                             └──┘ └─┘   └─┘   └─┘      └─────────────┘ └─┘
doc    └──┘                     └──┘ └─┘    └─┘   └─┘
542  
543  @[simp] theorem join_cons_nil (a : α) (S) :
id                                      
typ                                     
doc    └──┘
544    join (cons (a, nil) S) = cons a (join S) :=
id     └──┘  └──┘   └─┘     └──┘   └──┘ 
src    └──┘  └──┘    └─┘      └──┘    └──┘
typ    └──┘  └──┘   └─┘     └──┘   └──┘ 
doc    └──┘  └──┘     └─┘       └──┘    └──┘
545  destruct_eq_cons $ by simp [join]
id   └──────────────┘            └──┘
src  └──────────────┘      └────┘└──┘└─
typ  └──────────────┘      └────┘└──┘└─
doc                        └────┘└──┘└─
txt                        └────┘    └─
par                        └────┘    └─
pid                                
st                        └────────────
546  
src  
typ  
doc  
txt  
par  
pid  
st   
547  @[simp] theorem join_cons_cons (a b : α) (s S) :
id                                         
typ                                        
doc    └──┘
548    join (cons (a, cons b s) S) = cons a (join (cons (b, s) S)) :=
id     └──┘  └──┘   └──┘       └──┘   └──┘  └──┘     
src    └──┘  └──┘    └──┘          └──┘    └──┘  └──┘ 
typ    └──┘  └──┘   └──┘       └──┘   └──┘  └──┘     
doc    └──┘  └──┘     └──┘           └──┘    └──┘  └──┘
549  destruct_eq_cons $ by simp [join]
id   └──────────────┘            └──┘
src  └──────────────┘      └────┘└──┘└─
typ  └──────────────┘      └────┘└──┘└─
doc                        └────┘└──┘└─
txt                        └────┘    └─
par                        └────┘    └─
pid                                
st                        └────────────
550  
src  
typ  
doc  
txt  
par  
pid  
st   
551  @[simp] theorem join_cons (a : α) (s S) :
id                                  
typ                                 
doc    └──┘
552    join (cons (a, s) S) = cons a (append s (join S)) :=
id     └──┘  └──┘        └──┘   └────┘   └──┘ 
src    └──┘  └──┘           └──┘    └────┘    └──┘
typ    └──┘  └──┘        └──┘   └────┘   └──┘ 
doc    └──┘  └──┘             └──┘    └────┘    └──┘
553  begin
st   └─────
554    apply eq_of_bisim (λs1 s2, s1 = s2 ∨
id           └─────────┘                 
src    └────┘└─────────┘  └─────┘    
typ    └────┘└─────────┘  └─────┘    
doc    └────┘             └─────┘      
txt    └────┘             └─────┘      
par    └────┘             └─────┘      
pid                      └─────┘      
st   ───────────────────────────────────────
555      ∃ a s S, s1 = join (cons (a, s) S) ∧
id                                       
src  ───┘└────┘             └┘ └┘ └┘
typ  ───┘└────┘             └┘ └┘ └┘
doc  ───┘ └────┘               └┘ └┘ └┘ 
txt  ───┘ └────┘               └┘ └┘ └┘ 
par  ───┘ └────┘               └┘ └┘ └┘ 
pid  ───┘ └────┘               └┘ └┘ └┘ 
st   ─────────────────────────────────────────
556        s2 = cons a (append s (join S))) _ (or.inr ⟨a, s, S, rfl, rfl⟩),
id              └──┘    └────┘    └──┘         └────┘             └─┘
src  ─────┘   └──┘  └────┘  └──┘ └────┘ └────┘  └┘ └┘ └┘   └┘└─┘└┘
typ  ─────┘   └──┘  └────┘  └──┘ └────┘ └────┘ └┘└┘└┘   └┘└─┘└┘
doc  ─────┘   └──┘  └────┘  └──┘ └────┘         └┘ └┘ └┘   └┘   └┘
txt  ─────┘                      └────┘         └┘ └┘ └┘   └┘   └┘
par  ─────┘                      └────┘         └┘ └┘ └┘   └┘   └┘
pid  ─────┘                      └────┘         └┘ └┘ └┘   └┘   └┘
st   ────────────────────────────────────────────────────────────────────┘└─
557    intros s1 s2 h,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid          └──────┘
st   ───────────────┘└─
558    exact match s1, s2, h with
id                 └┘  └┘  
src    └────┘       └┘  └┘ └─────
typ    └────┘     └┘└┘└┘└┘└─────
doc    └────┘       └┘  └┘ └─────
txt    └────┘       └┘  └┘ └─────
par    └────┘       └┘  └┘ └─────
pid                └┘  └┘ └─────
st   ─────────────────────────────
559    | _, _, (or.inl $ eq.refl s) := begin
id              └────┘   └─────┘
src  ─────────┘ └────┘ └─────┘ └───┘     
typ  ─────────┘ └────┘ └─────┘ └───┘     
doc  ─────────┘                └───┘     
txt  ─────────┘                └───┘     
par  ─────────┘                └───┘     
pid  ─────────┘                └───┘     
st   ─────────────────────────────────┘└─────
560        apply cases_on s, { trivial },
id               └──────┘ 
src  ─────┘└────┘└──────┘ └──┘└──────┘└──
typ  ───────────┘└──────┘└──┘└──────┘└──
doc  ─────┘└────┘         └──┘└──────┘└──
txt  ─────┘└────┘         └──┘└──────┘└──
par  ───────────┘         └──┘└──────┘└──
pid  ───────────┘         └──────────────
st   ─────────────────────┘└─┘└───────┘└─
561        { intros x s, rw [destruct_cons], exact ⟨rfl, or.inl rfl⟩ }
id                           └───────────┘               └────┘ └─┘
src  ───────┘└────────┘└┘└──┘└───────────┘└──────┘    └┘└────┘└─┘└───
typ  ───────┘└────────┘└┘└──┘└───────────┘└──────┘    └┘└────┘└─┘└───
doc  ───────┘└────────┘└┘└──┘             └──────┘    └┘         └───
txt  ───────┘└────────┘└┘└──┘             └──────┘    └┘         └───
par  ───────┘└────────┘└┘└──┘             └──────┘    └┘         └───
pid  ───────────────────────┘             └───────┘    └┘         └───
st   ─────────────────┘└─────────────────┘└─────────────────────────┘└─
562      end
src  ────────
typ  ────────
doc  ────────
txt  ────────
par  ────────
pid  ────────
st   ──────┘
563    | ._, ._, (or.inr ⟨a, s, S, rfl, rfl⟩) := begin
src  ───┘  └┘  └┘         └┘ └┘ └┘   └┘   └────┘     
typ  ───┘  └┘  └┘         └┘ └┘ └┘   └┘   └────┘     
doc  ───┘  └┘  └┘         └┘ └┘ └┘   └┘   └────┘     
txt  ───┘  └┘  └┘         └┘ └┘ └┘   └┘   └────┘     
par  ───┘  └┘  └┘         └┘ └┘ └┘   └┘   └────┘     
pid  ───┘  └┘  └┘         └┘ └┘ └┘   └┘   └────┘     
st   ───────────────────────────────────────────┘└─────
564        apply cases_on s,
id               └──────┘ 
src  ─────┘└────┘└──────┘ └─
typ  ───────────┘└──────┘└─
doc  ─────┘└────┘         └─
txt  ─────┘└────┘         └─
par  ───────────┘         └─
pid  ───────────┘         └─
st   ─────────────────────┘└─
565        { simp },
src  ───────┘└───┘└──
typ  ───────┘└───┘└──
doc  ───────┘└───┘└──
txt  ───────┘└───┘└──
par  ───────┘└───┘└──
pid  ────────────────
st   ──────┘└────┘└─
566        { intros x s, simp, refine or.inr ⟨x, s, S, rfl, rfl⟩ }
id                                    └────┘             └─┘
src  ───────┘└────────┘└┘└──┘└┘└─────┘└────┘  └┘ └┘ └┘   └┘└─┘└┘└─
typ  ───────┘└────────┘└┘└──┘└───────┘└────┘ └┘└┘└┘   └┘└─┘└───
doc  ───────┘└────────┘└┘└──┘└┘└─────┘        └┘ └┘ └┘   └┘   └┘└─
txt  ───────┘└────────┘└┘└──┘└┘└─────┘        └┘ └┘ └┘   └┘   └┘└─
par  ───────┘└────────┘└┘└──┘└───────┘        └┘ └┘ └┘   └┘   └───
pid  ────────────────────────────────┘        └┘ └┘ └┘   └┘   └───
st   ─────────────────┘└────┘└──────────────────────────────────┘└─
567      end
src  ────────
typ  ────────
doc  ────────
txt  ────────
par  ────────
pid  ────────
st   ──────┘
568    end
src  ─────┘
typ  ─────┘
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ────┘
st   ─────┘
569  end
st   └─┘
570  
571  @[simp] theorem join_append (S T : seq (seq1 α)) :
id                                      └─┘  └──┘ 
src                                     └─┘  └──┘
typ                                     └─┘  └──┘ 
doc    └──┘                             └─┘  └──┘
572    join (append S T) = append (join S) (join T) :=
id     └──┘  └────┘     └────┘  └──┘    └──┘ 
src    └──┘  └────┘       └────┘  └──┘     └──┘
typ    └──┘  └────┘     └────┘  └──┘    └──┘ 
doc    └──┘  └────┘        └────┘  └──┘     └──┘
573  begin
st   └─────
574    apply eq_of_bisim (λs1 s2, ∃ s S T,
id           └─────────┘                
src    └────┘└─────────┘  └─────┘└────┘
typ    └────┘└─────────┘  └─────┘└────┘
doc    └────┘             └─────┘ └────┘ 
txt    └────┘             └─────┘ └────┘ 
par    └────┘             └─────┘ └────┘ 
pid                      └─────┘ └────┘ 
st   ──────────────────────────────────────
575      s1 = append s (join (append S T)) ∧
id                                        
src  ───┘                       └─┘
typ  ───┘                       └─┘
doc  ───┘                        └─┘ 
txt  ───┘                        └─┘ 
par  ───┘                        └─┘ 
pid  ───┘                        └─┘ 
st   ────────────────────────────────────────
576      s2 = append s (append (join S) (join T))),
id                      └────┘           └──┘
src  ───┘           └────┘      └┘ └──┘ └─┘
typ  ───┘           └────┘      └┘ └──┘ └─┘
doc  ───┘           └────┘      └┘ └──┘ └─┘
txt  ───┘                       └┘      └─┘
par  ───┘                       └┘      └─┘
pid  ───┘                       └┘      └─┘
st   ────────────────────────────────────────────┘└─
577    { intros s1 s2 h, exact match s1, s2, h with ._, ._, ⟨s, S, T, rfl, rfl⟩ := begin
id                                   └┘  └┘                               └─┘
src      └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘ └┘   └┘└─┘└───┘     
typ      └────────────┘  └────┘     └┘└┘└┘└┘└────┘  └┘  └┘  └┘ └┘ └┘   └┘└─┘└───┘     
doc      └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘ └┘   └┘   └───┘     
txt      └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘ └┘   └┘   └───┘     
par      └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘ └┘   └┘   └───┘     
pid            └──────┘              └┘  └┘ └────┘  └┘  └┘  └┘ └┘ └┘   └┘   └───┘     
st   ───┘└────────────┘└──────────────────────────────────────────────────────────┘└─────
578        apply cases_on s; simp,
id               └──────┘ 
src  ─────┘└────┘└──────┘ └┘└──┘└─
typ  ───────────┘└──────┘└┘└──┘└─
doc  ─────┘└────┘         └┘└──┘└─
txt  ─────┘└────┘         └┘└──┘└─
par  ───────────┘         └┘└──┘└─
pid  ───────────┘         └───────
st   ───────────────────────────┘└─
579        { apply cases_on S; simp,
id                 └──────┘ 
src  ───────┘└────┘└──────┘ └┘└──┘└─
typ  ─────────────┘└──────┘└┘└──┘└─
doc  ───────┘└────┘         └┘└──┘└─
txt  ───────┘└────┘         └┘└──┘└─
par  ─────────────┘         └┘└──┘└─
pid  ─────────────┘         └───────
st   ──────┘└─────────────────────┘└─
580          { apply cases_on T, { simp },
id                   └──────┘ 
src  ─────────┘└────┘└──────┘ └──┘└───┘└──
typ  ───────────────┘└──────┘└──┘└───┘└──
doc  ─────────┘└────┘         └──┘└───┘└──
txt  ─────────┘└────┘         └──┘└───┘└──
par  ───────────────┘         └──┘└───┘└──
pid  ───────────────┘         └───────────
st   ────────┘└───────────────┘└─┘└────┘└─
581            { intros s T, cases s with a s; simp,
id                                 
src  ───────────┘└────────┘└┘└────┘ └───────┘└┘└──┘└─
typ  ───────────┘└────────┘└┘└────┘└───────┘└┘└──┘└─
doc  ───────────┘└────────┘└┘└────┘ └───────┘└┘└──┘└─
txt  ───────────┘└────────┘└┘└────┘ └───────┘└┘└──┘└─
par  ───────────┘└────────┘└┘└────┘ └───────┘└┘└──┘└─
pid  ─────────────────────────────┘ └────────────────
st   ─────────────────────┘└──────────────────────┘└─
582              refine ⟨s, nil, T, _, _⟩; simp } },
id                         └─┘  
src  ───────────┘└─────┘  └┘└─┘└┘ └─────┘└┘└───┘└────
typ  ──────────────────┘ └┘└─┘└┘└───────┘└───┘└────
doc  ───────────┘└─────┘  └┘└─┘└┘ └─────┘└┘└───┘└────
txt  ───────────┘└─────┘  └┘   └┘ └─────┘└┘└───┘└────
par  ──────────────────┘  └┘   └┘ └───────┘└───┘└────
pid  ──────────────────┘  └┘   └┘ └──────────────────
st   ──────────────────────────────────────────┘└─┘└─
583          { intros s S, cases s with a s; simp,
id                               
src  ─────────┘└────────┘└┘└────┘ └───────┘└┘└──┘└─
typ  ─────────┘└────────┘└┘└────┘└───────┘└┘└──┘└─
doc  ─────────┘└────────┘└┘└────┘ └───────┘└┘└──┘└─
txt  ─────────┘└────────┘└┘└────┘ └───────┘└┘└──┘└─
par  ─────────┘└────────┘└┘└────┘ └───────┘└┘└──┘└─
pid  ───────────────────────────┘ └────────────────
st   ───────────────────┘└──────────────────────┘└─
584            exact ⟨s, S, T, rfl, rfl⟩ } },
id                               └─┘
src  ───────────────┘  └┘ └┘ └┘   └┘└─┘└──────
typ  ───────────────┘ └┘└┘└┘   └┘└─┘└──────
doc  ───────────────┘  └┘ └┘ └┘   └┘   └──────
txt  ───────────────┘  └┘ └┘ └┘   └┘   └──────
par  ───────────────┘  └┘ └┘ └┘   └┘   └──────
pid  ───────────────┘  └┘ └┘ └┘   └┘   └──────
st   ───────────────────────────────────┘└─┘└─
585        { intros x s, exact ⟨s, S, T, rfl, rfl⟩ }
id                                         └─┘
src  ───────┘└────────┘└──────┘  └┘ └┘ └┘   └┘└─┘└───
typ  ───────┘└────────┘└──────┘ └┘└┘└┘   └┘└─┘└───
doc  ───────┘└────────┘└──────┘  └┘ └┘ └┘   └┘   └───
txt  ───────┘└────────┘└──────┘  └┘ └┘ └┘   └┘   └───
par  ───────┘└────────┘└──────┘  └┘ └┘ └┘   └┘   └───
pid  ─────────────────────────┘  └┘ └┘ └┘   └┘   └───
st   ─────────────────┘└──────────────────────────┘└─
586      end end },
src  ───────────┘
typ  ───────────┘
doc  ───────────┘
txt  ───────────┘
par  ───────────┘
pid  ──────────┘
st   ──────┘└───┘└┘
587    { refine ⟨nil, S, T, _, _⟩; simp }
id               └─┘    
src      └─────┘ └─┘└┘ └┘ └─────┘  └───┘
typ      └─────┘ └─┘└┘└┘└─────┘  └───┘
doc      └─────┘ └─┘└┘ └┘ └─────┘  └───┘
txt      └─────┘    └┘ └┘ └─────┘  └───┘
par      └─────┘    └┘ └┘ └─────┘  └───┘
pid                └┘ └┘ └─────┘      
st   ──────────────────────────────────┘└─
588  end
st   ──┘
589  
590  @[simp] theorem of_list_nil : of_list [] = (nil : seq α) := rfl
id                                 └─────┘ └┘   └─┘   └─┘      └─┘
src                                └─────┘ └┘   └─┘   └─┘       └─┘
typ                                └─────┘ └┘   └─┘   └─┘      └─┘
doc    └──┘                        └─────┘       └─┘   └─┘
591  
592  @[simp] theorem of_list_cons (a : α) (l) :
id                                     
typ                                    
doc    └──┘
593    of_list (a :: l) = cons a (of_list l) :=
id     └─────┘   └┘    └──┘   └─────┘ 
src    └─────┘    └┘     └──┘    └─────┘
typ    └─────┘   └┘    └──┘   └─────┘ 
doc    └─────┘            └──┘    └─────┘
594  begin
st   └─────
595    apply subtype.eq, simp [of_list, cons],
id           └────────┘        └─────┘  └──┘
src    └────┘└────────┘  └────┘└─────┘└┘└──┘
typ    └────┘└────────┘  └────┘└─────┘└┘└──┘
doc    └────┘            └────┘└─────┘└┘└──┘
txt    └────┘            └────┘       └┘    
par    └────┘            └────┘       └┘    
pid                                └┘    
st   ─────────────────┘└────────────────────┘└─
596    funext n, cases n; simp [list.nth, stream.cons]
id                             └──────┘  └─────────┘
src    └──────┘  └────┘   └────┘└──────┘└┘└─────────┘└┘
typ    └──────┘  └────┘  └────┘└──────┘└┘└─────────┘└┘
doc    └──────┘  └────┘   └────┘        └┘           └┘
txt    └──────┘  └────┘   └────┘        └┘           └┘
par    └──────┘  └────┘   └────┘        └┘           └┘
pid          └┘                      └┘           
st   ─────────┘└──────────────────────────────────────┘
597  end
st   └─┘
598  
599  @[simp] theorem of_stream_cons (a : α) (s) :
id                                       
typ                                      
doc    └──┘
600    of_stream (a :: s) = cons a (of_stream s) :=
id     └───────┘   └┘    └──┘   └───────┘ 
src    └───────┘    └┘     └──┘    └───────┘
typ    └───────┘   └┘    └──┘   └───────┘ 
doc    └───────┘            └──┘    └───────┘
601  by apply subtype.eq; simp [of_stream, cons]; rw stream.map_cons
id            └────────┘        └───────┘  └──┘      └─────────────┘
src     └────┘└────────┘  └────┘└───────┘└┘└──┘  └─┘└─────────────┘
typ     └────┘└────────┘  └────┘└───────┘└┘└──┘  └─┘└─────────────┘
doc     └────┘            └────┘└───────┘└┘└──┘  └─┘               
txt     └────┘            └────┘         └┘      └─┘               
par     └────┘            └────┘         └┘      └─┘               
pid                                   └┘                       
st     └────────────────────────────────────────────┘└─────────────┘
602  
src  
typ  
doc  
txt  
par  
pid  
st   
603  @[simp] theorem of_list_append (l l' : list α) :
id                                          └──┘ 
src                                         └──┘
typ                                         └──┘ 
doc    └──┘
604    of_list (l ++ l') = append (of_list l) (of_list l') :=
id     └─────┘   └┘ └┘   └────┘  └─────┘    └─────┘ └┘
src    └─────┘    └┘      └────┘  └─────┘     └─────┘
typ    └─────┘   └┘ └┘   └────┘  └─────┘    └─────┘ └┘
doc    └─────┘             └────┘  └─────┘     └─────┘
605  by induction l; simp [*]
id                
src     └────────┘   └────────
typ     └────────┘  └────────
doc     └────────┘   └────────
txt     └────────┘   └────────
par     └────────┘   └────────
pid                     └─┘
st     └──────────────────────
606  
src  
typ  
doc  
txt  
par  
pid  
st   
607  @[simp] theorem of_stream_append (l : list α) (s : stream α) :
id                                         └──┘        └────┘ 
src                                        └──┘         └────┘
typ                                        └──┘        └────┘ 
doc    └──┘
608    of_stream (l ++ₛ s) = append (of_list l) (of_stream s) :=
id     └───────┘   └─┘    └────┘  └─────┘    └───────┘ 
src    └───────┘    └─┘     └────┘  └─────┘     └───────┘
typ    └───────┘   └─┘    └────┘  └─────┘    └───────┘ 
doc    └───────┘             └────┘  └─────┘     └───────┘
609  by induction l; simp [*, stream.nil_append_stream, stream.cons_append_stream]
id                           └──────────────────────┘  └───────────────────────┘
src     └────────┘   └───────┘└──────────────────────┘└┘└───────────────────────┘└─
typ     └────────┘  └───────┘└──────────────────────┘└┘└───────────────────────┘└─
doc     └────────┘   └───────┘                        └┘                         └─
txt     └────────┘   └───────┘                        └┘                         └─
par     └────────┘   └───────┘                        └┘                         └─
pid                     └──┘                        └┘                         
st     └───────────────────────────────────────────────────────────────────────────
610  
src  
typ  
doc  
txt  
par  
pid  
st   
611  /-- Convert a sequence into a list, embedded in a computation to allow for
612    the possibility of infinite sequences (in which case the computation
613    never returns anything). -/
614  def to_list' {α} (s : seq α) : computation (list α) :=
id                         └─┘     └─────────┘  └──┘ 
src                        └─┘      └─────────┘  └──┘
typ                        └─┘     └─────────┘  └──┘ 
doc                        └─┘      └─────────┘
615  @computation.corec (list α) (list α × seq α) (λ⟨l, s⟩,
id    └───────────────┘  └──┘    └──┘   └─┘       
src   └───────────────┘  └──┘     └──┘    └─┘
typ   └───────────────┘  └──┘    └──┘   └─┘       
doc   └───────────────┘                    └─┘
616    match destruct s with
id           └──────┘
src          └──────┘
typ          └──────┘
doc          └──────┘
617    | none         := sum.inl l.reverse
id       └──┘            └─────┘  └──────┘
src      └──┘            └─────┘  └──────┘
typ      └──┘            └─────┘  └──────┘
618    | some (a, s') := sum.inr (a::l, s')
id       └──┘   └┘     └─────┘  └┘
src      └──┘           └─────┘  └┘
typ      └──┘   └┘     └─────┘  └┘
619    end) ([], s)
id          └┘  
src         └┘
typ         └┘  
620  
621  theorem dropn_add (s : seq α) (m) : ∀ n, drop s (m + n) = drop (drop s m) n
id                          └─┘             └──┘        └──┘  └──┘    
src                         └─┘               └──┘           └──┘  └──┘
typ                         └─┘             └──┘        └──┘  └──┘    
doc                         └─┘               └──┘             └──┘  └──┘
622  | 0     := rfl
id              └─┘
src             └─┘
typ             └─┘
623  | (n+1) := congr_arg tail (dropn_add n)
id            └───────┘ └──┘  └───────┘
src            └───────┘ └──┘
typ           └───────┘ └──┘  └───────┘
doc                       └──┘
624  
625  theorem dropn_tail (s : seq α) (n) : drop (tail s) n = drop s (n + 1) :=
id                           └─┘         └──┘  └──┘     └──┘    
src                          └─┘          └──┘  └──┘       └──┘      
typ                          └─┘         └──┘  └──┘     └──┘    
doc                          └─┘          └──┘  └──┘        └──┘
626  by rw add_comm; symmetry; apply dropn_add
id         └──────┘                  └───────┘
src     └─┘└──────┘  └──────┘  └────┘└───────┘
typ     └─┘└──────┘  └──────┘  └────┘└───────┘
doc     └─┘          └──────┘  └────┘         
txt     └─┘          └──────┘  └────┘         
par     └─┘          └──────┘  └────┘         
pid                                         
st     └───────────────────────────────────────
627  
src  
typ  
doc  
txt  
par  
pid  
st   
628  theorem nth_tail : ∀ (s : seq α) n, nth (tail s) n = nth s (n + 1)
id                            └─┘     └─┘  └──┘     └─┘    
src                            └─┘       └─┘  └──┘       └─┘      
typ                           └─┘     └─┘  └──┘     └─┘    
doc                            └─┘       └─┘  └──┘        └─┘
629  | ⟨f, al⟩ n := rfl
id                  └─┘
src                 └─┘
typ                 └─┘
630  
631  @[ext]
doc    └─┘
632  protected lemma ext (s s': seq α) (hyp : ∀ (n : ℕ), s.nth n = s'.nth n) : s = s' :=
id                              └─┘                    └──┘   └┘└──┘       └┘
src                             └─┘                      └──┘      └──┘        
typ                             └─┘                    └──┘   └┘└──┘       └┘
doc                             └─┘                       └──┘       └──┘
633  begin
st   └─────
634    let ext := (λ (s s' : seq α), ∀ n, s.nth n = s'.nth n),
id                           └─┘          └──┘      └──┘
src    └─────────┘  └───────┘└─┘ └─┘ └┘  └──┘   └──┘ 
typ    └─────────┘  └───────┘└─┘└─┘ └┘  └──┘   └──┘ 
doc    └─────────┘  └───────┘└─┘ └─┘ └┘  └──┘    └──┘ 
txt    └─────────┘  └───────┘    └─┘ └┘               
par    └─────────┘  └───────┘    └─┘ └┘               
pid    └─────┘└─┘  └───────┘    └─┘ └┘               
st   ───────────────────────────────────────────────────────┘└─
635    apply seq.eq_of_bisim ext _ hyp,
id           └─────────────┘ └─┘   └─┘
src    └────┘└─────────────┘   └─┘
typ    └────┘└─────────────┘└─┘└─┘└─┘
doc    └────┘                  └─┘
txt    └────┘                  └─┘
par    └────┘                  └─┘
pid                           └─┘
st   ────────────────────────────────┘└─
636    -- we have to show that ext is a bisimulation
st   ────────────────────────────────────────────────
637    clear hyp s s',
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid         └───────┘
st   ───────────────┘└─
638    assume s s' (hyp : ext s s'),
id                        └─┘  └┘
src    └─────────────────┘      
typ    └─────────────────┘└─┘└┘
doc    └─────────────────┘      
txt    └─────────────────┘      
par    └─────────────────┘      
pid    └─────────────────┘      
st   ─────────────────────────────┘└─
639    unfold seq.destruct,
src    └─────────────────┘
typ    └─────────────────┘
doc    └─────────────────┘
txt    └─────────────────┘
par    └─────────────────┘
pid          └───────────┘
st   ────────────────────┘└─
640    rw (hyp 0),
id         └─┘
src    └─┘    └─┘
typ    └─┘ └─┘└─┘
doc    └─┘    └─┘
txt    └─┘    └─┘
par    └─┘    └─┘
pid          └─┘
st   ───────────┘└─
641    cases (s'.nth 0),
id            └────┘
src    └────┘ └────┘└─┘
typ    └────┘ └────┘└─┘
doc    └────┘ └────┘└─┘
txt    └────┘       └─┘
par    └────┘       └─┘
pid                └─┘
st   ─────────────────┘└─
642    { simp [seq.bisim_o] }, -- option.none
id             └─────────┘
src      └────┘└─────────┘└┘
typ      └────┘└─────────┘└┘
doc      └────┘           └┘
txt      └────┘           └┘
par      └────┘           └┘
pid                     
st   ───┘└─────────────────┘└┘└───────────────
643    { -- option.some
st   ───────────────────
644      suffices : ext s.tail s'.tail, by simpa,
id                  └─┘ └────┘ └─────┘
src      └─────────┘   └────┘└─────┘     └───┘
typ      └─────────┘└─┘└────┘└─────┘     └───┘
doc      └─────────┘   └────┘└─────┘     └───┘
txt      └─────────┘                     └───┘
par      └─────────┘                     └───┘
pid      └───────┘└┘         
st   ────────────────────────────────┘          └─
645      assume n,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───────────┘└─
646      simp only [seq.nth_tail _ n, (hyp $ n + 1)] }
id                  └──────────┘      └─┘    
src      └─────────┘└──────────┘└─┘ └┘      └───┘
typ      └─────────┘└──────────┘└─┘└┘ └─┘ └───┘
doc      └─────────┘            └─┘ └┘       └───┘
txt      └─────────┘            └─┘ └┘       └───┘
par      └─────────┘            └─┘ └┘       └───┘
pid          └──┘└┘            └─┘ └┘       └──┘
st   ───────────────────────────────────────────────┘└─
647  end
st   ──┘
648  
649  @[simp] theorem head_dropn (s : seq α) (n) : head (drop s n) = nth s n :=
id                                   └─┘         └──┘  └──┘     └─┘  
src                                  └─┘          └──┘  └──┘       └─┘
typ                                  └─┘         └──┘  └──┘     └─┘  
doc    └──┘                          └─┘          └──┘  └──┘        └─┘
650  begin
st   └─────
651    induction n with n IH generalizing s, { refl },
id               
src    └────────┘ └───────────────────────┘    └───┘
typ    └────────┘└───────────────────────┘    └───┘
doc    └────────┘ └───────────────────────┘    └───┘
txt    └────────┘ └───────────────────────┘    └───┘
par    └────────┘ └───────────────────────┘    └───┘
pid              └───────┘└─────────────┘        
st   ─────────────────────────────────────┘└──┘└───┘└┘
652    rw [nat.succ_eq_add_one, ←nth_tail, ←dropn_tail], apply IH
id         └─────────────────┘   └──────┘   └────────┘
src    └──┘└─────────────────┘└─┘└──────┘└─┘└────────┘  └────┘  
typ    └──┘└─────────────────┘└─┘└──────┘└─┘└────────┘  └────┘  
doc    └──┘                   └─┘        └─┘            └────┘  
txt    └──┘                   └─┘        └─┘            └────┘  
par    └──┘                   └─┘        └─┘            └────┘  
pid      └┘                   └─┘        └─┘                   
st   ────────────────────────┘└─────────┘└───────────┘└─────────┘
653  end
st   └─┘
654  
655  theorem mem_map (f : α → β) {a : α} : ∀ {s : seq α}, a ∈ s → f a ∈ map f s
id                                            └─┘            └─┘  
src                                               └─┘                 └─┘
typ                                           └─┘            └─┘  
doc                                               └─┘                   └─┘
656  | ⟨g, al⟩ := stream.mem_map (option.map f)
id                └────────────┘  └────────┘ 
src               └────────────┘  └────────┘
typ               └────────────┘  └────────┘ 
657  
658  theorem exists_of_mem_map {f} {b : β} : ∀ {s : seq α}, b ∈ map f s → ∃ a, a ∈ s ∧ f a = b
id                                                └─┘      └─┘              
src                                                 └─┘        └─┘                    
typ                                               └─┘      └─┘              
doc                                                 └─┘         └─┘
659  | ⟨g, al⟩ h := let ⟨o, om, oe⟩ := stream.exists_of_mem_map h in
id                 └─┘                └──────────────────────┘
src                                    └──────────────────────┘
typ                └─┘                └──────────────────────┘
660    by cases o with a; injection oe with h'; exact ⟨a, om, h'⟩
id                                 └┘                   └┘  └┘
src       └────┘ └─────┘  └────────┘  └──────┘  └────┘  └┘  └┘  └─
typ       └────┘└─────┘  └────────┘└┘└──────┘  └────┘ └┘└┘└┘└┘└─
doc       └────┘ └─────┘  └────────┘  └──────┘  └────┘  └┘  └┘  └─
txt       └────┘ └─────┘  └────────┘  └──────┘  └────┘  └┘  └┘  └─
par       └────┘ └─────┘  └────────┘  └──────┘  └────┘  └┘  └┘  └─
pid             └─────┘             └──────┘         └┘  └┘  
st       └────────────────────────────────────────────────────────
661  
src  
typ  
doc  
txt  
par  
pid  
st   
662  theorem of_mem_append {s₁ s₂ : seq α} {a : α} (h : a ∈ append s₁ s₂) : a ∈ s₁ ∨ a ∈ s₂ :=
id                                  └─┘                 └────┘ └┘ └┘      └┘    └┘
src                                 └─┘                    └────┘                   
typ                                 └─┘                 └────┘ └┘ └┘      └┘    └┘
doc                                 └─┘                     └────┘
663  begin
st   └─────
664    have := h, revert this,
id             
src    └──────┘   └─────────┘
typ    └──────┘  └─────────┘
doc    └──────┘   └─────────┘
txt    └──────┘   └─────────┘
par    └──────┘   └─────────┘
pid    └───┘└─┘         └───┘
st   ──────────┘└───────────┘└─
665    generalize e : append s₁ s₂ = ss, intro h, revert s₁,
id                    └────┘ └┘ └┘
src    └─────────────┘└────┘         └─────┘  └───────┘
typ    └─────────────┘└────┘└┘└┘     └─────┘  └───────┘
doc    └─────────────┘└────┘         └─────┘  └───────┘
txt    └─────────────┘               └─────┘  └───────┘
par    └─────────────┘               └─────┘  └───────┘
pid              └┘└┘                    └┘        └─┘
st   ─────────────────────────────────┘└───────┘└─────────┘└─
666    apply mem_rec_on h _,
id           └────────┘ 
src    └────┘└────────┘ └┘
typ    └────┘└────────┘└┘
doc    └────┘           └┘
txt    └────┘           └┘
par    └────┘           └┘
pid                    └┘
st   ─────────────────────┘└─
667    intros b s' o s₁,
src    └──────────────┘
typ    └──────────────┘
doc    └──────────────┘
txt    └──────────────┘
par    └──────────────┘
pid          └────────┘
st   ─────────────────┘└─
668    apply s₁.cases_on _ (λ c t₁, _); intros m e;
id           └─────────┘
src    └────┘└─────────┘└─┘  └───────┘  └────────┘
typ    └────┘└─────────┘└─┘  └───────┘  └────────┘
doc    └────┘           └─┘  └───────┘  └────────┘
txt    └────┘           └─┘  └───────┘  └────────┘
par    └────┘           └─┘  └───────┘  └────────┘
pid                    └─┘  └───────┘        └──┘
st   ───────────────────────────────────────────────
669    have := congr_arg destruct e,
id             └───────┘ └──────┘ 
src    └──────┘└───────┘└──────┘
typ    └──────┘└───────┘└──────┘
doc    └──────┘         └──────┘
txt    └──────┘                 
par    └──────┘                 
pid    └───┘└─┘                 
st   ─────────────────────────────┘└─
670    { apply or.inr, simpa using m },
id             └────┘              
src      └────┘└────┘  └──────────┘ 
typ      └────┘└────┘  └──────────┘
doc      └────┘        └──────────┘ 
txt      └────┘        └──────────┘ 
par      └────┘        └──────────┘ 
pid                        └────┘ 
st   ───┘└──────────┘└──────────────┘└┘
671    { cases (show a = c ∨ a ∈ append t₁ s₂, by simpa using m) with e' m,
id                           └────┘ └┘ └┘                 
src      └────┘          └────┘    └───┘└──────────┘ └─────────┘
typ      └────┘       └────┘└┘└┘└───┘└──────────┘└─────────┘
doc      └────┘           └────┘    └───┘└──────────┘ └─────────┘
txt      └────┘                     └───┘└──────────┘ └─────────┘
par      └────┘                     └───┘└──────────┘ └─────────┘
pid                                └───────────────┘ └────────┘
st   ───────────────────────────────────────────┘└────────────┘└─────────┘└─
672      { rw e', exact or.inl (mem_cons _ _) },
id            └┘        └────┘  └──────┘
src        └─┘    └────┘└────┘ └──────┘└────┘
typ        └─┘└┘  └────┘└────┘ └──────┘└────┘
doc        └─┘    └────┘               └────┘
txt        └─┘    └────┘               └────┘
par        └─┘    └────┘               └────┘
pid                                  └───┘
st   ─────┘└───┘└────────────────────────────┘└┘
673      { cases (show c = b ∧ append t₁ s₂ = s', by simpa) with i1 i2,
id                          └────┘ └┘ └┘   └┘
src        └────┘         └────┘       └───┘└───┘└──────────┘
typ        └────┘      └────┘└┘└┘ └┘└───┘└───┘└──────────┘
doc        └────┘         └────┘       └───┘└───┘└──────────┘
txt        └────┘                      └───┘└───┘└──────────┘
par        └────┘                      └───┘└───┘└──────────┘
pid                                   └─────────┘└─────────┘
st   ──────────────────────────────────────────────┘└────┘└──────────┘└─
674        cases o with e' IH,
id               
src        └────┘ └─────────┘
typ        └────┘└─────────┘
doc        └────┘ └─────────┘
txt        └────┘ └─────────┘
par        └────┘ └─────────┘
pid              └─────────┘
st   ───────────────────────┘└─
675        { simp [i1, e'] },
id                 └┘  └┘
src          └────┘  └┘  └┘
typ          └────┘└┘└┘└┘└┘
doc          └────┘  └┘  └┘
txt          └────┘  └┘  └┘
par          └────┘  └┘  └┘
pid                └┘  
st   ───────┘└────────────┘└┘
676        { exact or.imp_left (mem_cons_of_mem _) (IH m i2) } } }
id                 └─────────┘  └─────────────┘     └┘  └┘
src          └────┘└─────────┘ └─────────────┘└──┘      └┘
typ          └────┘└─────────┘ └─────────────┘└──┘ └┘└┘└┘
doc          └────┘                           └──┘      └┘
txt          └────┘                           └──┘      └┘
par          └────┘                           └──┘      └┘
pid                                          └──┘      
st   ───────────────────────────────────────────────────────┘└─────
677  end
st   ──┘
678  
679  theorem mem_append_left {s₁ s₂ : seq α} {a : α} (h : a ∈ s₁) : a ∈ append s₁ s₂ :=
id                                    └─┘                 └┘      └────┘ └┘ └┘
src                                   └─┘                             └────┘
typ                                   └─┘                 └┘      └────┘ └┘ └┘
doc                                   └─┘                               └────┘
680  by apply mem_rec_on h; intros; simp [*]
id            └────────┘ 
src     └────┘└────────┘   └────┘  └────────
typ     └────┘└────────┘  └────┘  └────────
doc     └────┘             └────┘  └────────
txt     └────┘             └────┘  └────────
par     └────┘             └────┘  └────────
pid                                   └─┘
st     └─────────────────────────────────────
681  
src  
typ  
doc  
txt  
par  
pid  
st   
682  end seq
683  
684  namespace seq1
685  variables {α : Type u} {β : Type v} {γ : Type w}
686  open seq
687  
688  /-- Convert a `seq1` to a sequence. -/
689  def to_seq : seq1 α → seq α
id                └──┘   └─┘ 
src               └──┘     └─┘
typ               └──┘   └─┘ 
doc               └──┘     └─┘
690  | (a, s) := cons a s
id            └──┘
src             └──┘
typ           └──┘
doc              └──┘
691  
692  instance coe_seq : has_coe (seq1 α) (seq α) := ⟨to_seq⟩
id                      └─────┘  └──┘    └─┘       └────┘
src                     └─────┘  └──┘     └─┘        └────┘
typ                     └─────┘  └──┘    └─┘       └────┘
doc                              └──┘     └─┘        └────┘
693  
694  /-- Map a function on a `seq1` -/
695  def map (f : α → β) : seq1 α → seq1 β
id                       └──┘   └──┘ 
src                        └──┘     └──┘
typ                      └──┘   └──┘ 
doc                        └──┘     └──┘
696  | (a, s) := (f a, seq.map f s)
id                └─────┘ 
src                  └─────┘
typ               └─────┘ 
doc                    └─────┘
697  
698  theorem map_id : ∀ (s : seq1 α), map id s = s | ⟨a, s⟩ := by simp [map]
id                          └──┘    └─┘ └┘                         └─┘
src                          └──┘     └─┘ └┘                     └────┘└─┘└─
typ                         └──┘    └─┘ └┘                   └────┘└─┘└─
doc                          └──┘     └─┘                         └────┘└─┘└─
txt                                                               └────┘   └─
par                                                               └────┘   └─
pid                                                                      
st                                                               └───────────
699  
src  
typ  
doc  
txt  
par  
pid  
st   
700  /-- Flatten a nonempty sequence of nonempty sequences -/
701  def join : seq1 (seq1 α) → seq1 α
id              └──┘  └──┘    └──┘ 
src             └──┘  └──┘      └──┘
typ             └──┘  └──┘    └──┘ 
doc             └──┘  └──┘      └──┘
702  | ((a, s), S) := match destruct s with
id     └┘                └──────┘
src    └┘                   └──────┘
typ    └┘                └──────┘
doc                         └──────┘
703    | none := (a, seq.join S)
id       └──┘       └──────┘
src      └──┘       └──────┘
typ      └──┘       └──────┘
doc                  └──────┘
704    | some s' := (a, seq.join (cons s' S))
id       └──┘ └┘       └──────┘  └──┘
src      └──┘          └──────┘  └──┘
typ      └──┘ └┘       └──────┘  └──┘
doc                     └──────┘  └──┘
705    end
706  
707  @[simp] theorem join_nil (a : α) (S) : join ((a, nil), S) = (a, seq.join S) := rfl
id                                         └──┘ └┘  └─┘        └──────┘      └─┘
src                                         └──┘ └┘   └─┘          └──────┘       └─┘
typ                                        └──┘ └┘  └─┘        └──────┘      └─┘
doc    └──┘                                 └──┘      └─┘            └──────┘
708  
709  @[simp] theorem join_cons (a b : α) (s S) :
id                                    
typ                                   
doc    └──┘
710    join ((a, cons b s), S) = (a, seq.join (cons (b, s) S)) :=
id     └──┘ └┘  └──┘          └──────┘  └──┘     
src    └──┘ └┘   └──┘              └──────┘  └──┘ 
typ    └──┘ └┘  └──┘          └──────┘  └──┘     
doc    └──┘      └──┘                └──────┘  └──┘
711  by dsimp [join]; rw [destruct_cons]; refl
id             └──┘       └───────────┘
src     └─────┘└──┘  └──┘└───────────┘  └────
typ     └─────┘└──┘  └──┘└───────────┘  └────
doc     └─────┘└──┘  └──┘               └────
txt     └─────┘      └──┘               └────
par     └─────┘      └──┘               └────
pid                  └┘                   
st     └─────────────────┘└───────────┘└──────
712  
src  
typ  
doc  
txt  
par  
pid  
st   
713  /-- The `return` operator for the `seq1` monad,
714    which produces a singleton sequence. -/
715  def ret (a : α) : seq1 α := (a, nil)
id                    └──┘       └─┘
src                    └──┘         └─┘
typ                   └──┘       └─┘
doc                    └──┘          └─┘
716  
717  instance [inhabited α] : inhabited (seq1 α) := ⟨ret (default _)⟩
id             └───────┘     └───────┘  └──┘       └─┘  └─────┘
src            └───────┘      └───────┘  └──┘        └─┘  └─────┘
typ            └───────┘     └───────┘  └──┘       └─┘  └─────┘
doc                                      └──┘        └─┘
718  
719  /-- The `bind` operator for the `seq1` monad,
720    which maps `f` on each element of `s` and appends the results together.
721    (Not all of `s` may be evaluated, because the first few elements of `s`
722    may already produce an infinite result.) -/
723  def bind (s : seq1 α) (f : α → seq1 β) : seq1 β :=
id                 └──┘           └──┘     └──┘ 
src                └──┘             └──┘      └──┘
typ                └──┘           └──┘     └──┘ 
doc                └──┘             └──┘      └──┘
724  join (map f s)
id   └──┘  └─┘  
src  └──┘  └─┘
typ  └──┘  └─┘  
doc  └──┘  └─┘
725  
726  @[simp] theorem join_map_ret (s : seq α) : seq.join (seq.map ret s) = s :=
id                                     └─┘     └──────┘  └─────┘ └─┘    
src                                    └─┘      └──────┘  └─────┘ └─┘    
typ                                    └─┘     └──────┘  └─────┘ └─┘    
doc    └──┘                            └─┘      └──────┘  └─────┘ └─┘
727  by apply coinduction2 s; intro s; apply cases_on s; simp [ret]
id            └──────────┘                  └──────┘         └─┘
src     └────┘└──────────┘   └─────┘  └────┘└──────┘   └────┘└─┘└─
typ     └────┘└──────────┘  └─────┘  └────┘└──────┘  └────┘└─┘└─
doc     └────┘               └─────┘  └────┘           └────┘└─┘└─
txt     └────┘               └─────┘  └────┘           └────┘   └─
par     └────┘               └─────┘  └────┘           └────┘   └─
pid                              └┘                         
st     └────────────────────────────────────────────────────────────
728  
src  
typ  
doc  
txt  
par  
pid  
st   
729  @[simp] theorem bind_ret (f : α → β) : ∀ s, bind s (ret ∘ f) = map f s
id                                            └──┘   └─┘     └─┘  
src                                              └──┘    └─┘      └─┘
typ                                           └──┘   └─┘     └─┘  
doc    └──┘                                      └──┘    └─┘        └─┘
730  | ⟨a, s⟩ := begin
st               └─────
731    dsimp [bind, map], change (λx, ret (f x)) with (ret ∘ f),
id            └──┘  └─┘               └─┘             └─┘  
src    └─────┘└──┘└┘└─┘  └─────┘  └─┘└─┘   └──────┘ └─┘ 
typ    └─────┘└──┘└┘└─┘  └─────┘  └─┘└─┘  └──────┘ └─┘
doc    └─────┘└──┘└┘└─┘  └─────┘  └─┘└─┘   └──────┘ └─┘  
txt    └─────┘    └┘     └─────┘  └─┘      └──────┘      
par    └─────┘    └┘     └─────┘  └─┘      └──────┘      
pid             └┘             └─┘      └┘└────┘      
st   ──────────────────┘└────────────────────────────────────────
732    rw [map_comp], simp [function.comp, ret]
id         └──────┘         └───────────┘  └─┘
src    └──┘└──────┘  └────┘└───────────┘└┘└─┘└┘
typ    └──┘└──────┘  └────┘└───────────┘└┘└─┘└┘
doc    └──┘          └────┘             └┘└─┘└┘
txt    └──┘          └────┘             └┘   └┘
par    └──┘          └────┘             └┘   └┘
pid      └┘                           └┘   
st   ─────────────┘└───────────────────────────┘
733  end
st   └─┘
734  
735  @[simp] theorem ret_bind (a : α) (f : α → seq1 β) : bind (ret a) f = f a :=
id                                           └──┘     └──┘  └─┘      
src                                            └──┘      └──┘  └─┘      
typ                                          └──┘     └──┘  └─┘      
doc    └──┘                                    └──┘      └──┘  └─┘
736  begin
st   └─────
737    simp [ret, bind, map],
id           └─┘  └──┘  └─┘
src    └────┘└─┘└┘└──┘└┘└─┘
typ    └────┘└─┘└┘└──┘└┘└─┘
doc    └────┘└─┘└┘└──┘└┘└─┘
txt    └────┘   └┘    └┘   
par    └────┘   └┘    └┘   
pid           └┘    └┘   
st   ──────────────────────┘└─
738    cases f a with a s,
id            
src    └────┘  └───────┘
typ    └────┘└───────┘
doc    └────┘  └───────┘
txt    └────┘  └───────┘
par    └────┘  └───────┘
pid           └───────┘
st   ───────────────────┘└─
739    apply cases_on s; intros; simp
id           └──────┘ 
src    └────┘└──────┘   └────┘  └───┘
typ    └────┘└──────┘  └────┘  └───┘
doc    └────┘           └────┘  └───┘
txt    └────┘           └────┘  └───┘
par    └────┘           └────┘  └───┘
pid                                
st   ────────────────────────────────┘
740  end
st   └─┘
741  
742  @[simp] theorem map_join' (f : α → β) (S) :
id                                     
typ                                    
doc    └──┘
743    seq.map f (seq.join S) = seq.join (seq.map (map f) S) :=
id     └─────┘   └──────┘    └──────┘  └─────┘  └─┘   
src    └─────┘    └──────┘     └──────┘  └─────┘  └─┘
typ    └─────┘   └──────┘    └──────┘  └─────┘  └─┘   
doc    └─────┘    └──────┘      └──────┘  └─────┘  └─┘
744  begin
st   └─────
745    apply eq_of_bisim (λs1 s2,
id           └─────────┘
src    └────┘└─────────┘  └──────
typ    └────┘└─────────┘  └──────
doc    └────┘             └──────
txt    └────┘             └──────
par    └────┘             └──────
pid                      └──────
st   ─────────────────────────────
746      ∃ s S, s1 = append s (seq.map f (seq.join S)) ∧
id                                                  
src  ───┘└──┘                            └─┘
typ  ───┘└──┘                            └─┘
doc  ───┘ └──┘                              └─┘ 
txt  ───┘ └──┘                              └─┘ 
par  ───┘ └──┘                              └─┘ 
pid  ───┘ └──┘                              └─┘ 
st   ────────────────────────────────────────────────────
747        s2 = append s (seq.join (seq.map (map f) S))),
id              └────┘    └──────┘  └─────┘  └─┘ 
src  ─────┘   └────┘  └──────┘ └─────┘ └─┘ └┘ └─┘
typ  ─────┘   └────┘  └──────┘ └─────┘ └─┘└┘ └─┘
doc  ─────┘   └────┘  └──────┘ └─────┘ └─┘ └┘ └─┘
txt  ─────┘                                └┘ └─┘
par  ─────┘                                └┘ └─┘
pid  ─────┘                                └┘ └─┘
st   ──────────────────────────────────────────────────┘└─
748    { intros s1 s2 h, exact match s1, s2, h with ._, ._, ⟨s, S, rfl, rfl⟩ := begin
id                                   └┘  └┘                            └─┘
src      └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘   └┘└─┘└───┘     
typ      └────────────┘  └────┘     └┘└┘└┘└┘└────┘  └┘  └┘  └┘ └┘   └┘└─┘└───┘     
doc      └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘   └┘   └───┘     
txt      └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘   └┘   └───┘     
par      └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘ └┘   └┘   └───┘     
pid            └──────┘              └┘  └┘ └────┘  └┘  └┘  └┘ └┘   └┘   └───┘     
st   ───┘└────────────┘└───────────────────────────────────────────────────────┘└─────
749        apply cases_on s; simp,
id               └──────┘ 
src  ─────┘└────┘└──────┘ └┘└──┘└─
typ  ───────────┘└──────┘└┘└──┘└─
doc  ─────┘└────┘         └┘└──┘└─
txt  ─────┘└────┘         └┘└──┘└─
par  ───────────┘         └┘└──┘└─
pid  ───────────┘         └───────
st   ───────────────────────────┘└─
750        { apply cases_on S; simp,
id                 └──────┘ 
src  ───────┘└────┘└──────┘ └┘└──┘└─
typ  ─────────────┘└──────┘└┘└──┘└─
doc  ───────┘└────┘         └┘└──┘└─
txt  ───────┘└────┘         └┘└──┘└─
par  ─────────────┘         └┘└──┘└─
pid  ─────────────┘         └───────
st   ──────┘└─────────────────────┘└─
751          { intros x S, cases x with a s; simp [map],
id                                                └─┘
src  ─────────┘└────────┘└┘└────┘ └───────┘└┘└────┘└─┘└─
typ  ─────────┘└────────┘└┘└────┘└───────┘└┘└────┘└─┘└─
doc  ─────────┘└────────┘└┘└────┘ └───────┘└┘└────┘└─┘└─
txt  ─────────┘└────────┘└┘└────┘ └───────┘└┘└────┘   └─
par  ─────────┘└────────┘└┘└────┘ └───────┘└┘└────┘   └─
pid  ───────────────────────────┘ └───────────────┘   └──
st   ───────────────────┘└────────────────────────────┘└─
752            exact ⟨_, _, rfl, rfl⟩ } },
id                               └─┘
src  ───────────────┘ └────┘   └┘└─┘└──────
typ  ───────────────┘ └────┘   └┘└─┘└──────
doc  ───────────────┘ └────┘   └┘   └──────
txt  ───────────────┘ └────┘   └┘   └──────
par  ───────────────┘ └────┘   └┘   └──────
pid  ───────────────┘ └────┘   └┘   └──────
st   ────────────────────────────────┘└─┘└─
753        { intros x s, refine ⟨s, S, rfl, rfl⟩ }
id                                        └─┘
src  ───────┘└────────┘└┘└─────┘  └┘ └┘   └┘└─┘└┘└─
typ  ───────┘└────────┘└───────┘ └┘└┘   └┘└─┘└───
doc  ───────┘└────────┘└┘└─────┘  └┘ └┘   └┘   └┘└─
txt  ───────┘└────────┘└┘└─────┘  └┘ └┘   └┘   └┘└─
par  ───────┘└────────┘└───────┘  └┘ └┘   └┘   └───
pid  ──────────────────────────┘  └┘ └┘   └┘   └───
st   ─────────────────┘└────────────────────────┘└─
754      end end },
src  ───────────┘
typ  ───────────┘
doc  ───────────┘
txt  ───────────┘
par  ───────────┘
pid  ──────────┘
st   ──────┘└───┘└┘
755    { refine ⟨nil, S, _, _⟩; simp }
id               └─┘  
src      └─────┘ └─┘└┘ └─────┘  └───┘
typ      └─────┘ └─┘└┘└─────┘  └───┘
doc      └─────┘ └─┘└┘ └─────┘  └───┘
txt      └─────┘    └┘ └─────┘  └───┘
par      └─────┘    └┘ └─────┘  └───┘
pid                └┘ └─────┘      
st   ───────────────────────────────┘└─
756  end
st   ──┘
757  
758  @[simp] theorem map_join (f : α → β) : ∀ S, map f (join S) = join (map (map f) S)
id                                            └─┘   └──┘    └──┘  └─┘  └─┘   
src                                              └─┘    └──┘     └──┘  └─┘  └─┘
typ                                           └─┘   └──┘    └──┘  └─┘  └─┘   
doc    └──┘                                      └─┘    └──┘      └──┘  └─┘  └─┘
759  | ((a, s), S) := by apply cases_on s; intros; simp [map]
id     └┘                      └──────┘                 └─┘
src    └┘                └────┘└──────┘   └────┘  └────┘└─┘└─
typ    └┘                └────┘└──────┘  └────┘  └────┘└─┘└─
doc                      └────┘           └────┘  └────┘└─┘└─
txt                      └────┘           └────┘  └────┘   └─
par                      └────┘           └────┘  └────┘   └─
pid                                                     
st                      └─────────────────────────────────────
760  
src  
typ  
doc  
txt  
par  
pid  
st   
761  @[simp] theorem join_join (SS : seq (seq1 (seq1 α))) :
id                                   └─┘  └──┘  └──┘ 
src                                  └─┘  └──┘  └──┘
typ                                  └─┘  └──┘  └──┘ 
doc    └──┘                          └─┘  └──┘  └──┘
762    seq.join (seq.join SS) = seq.join (seq.map join SS) :=
id     └──────┘  └──────┘ └┘   └──────┘  └─────┘ └──┘ └┘
src    └──────┘  └──────┘      └──────┘  └─────┘ └──┘
typ    └──────┘  └──────┘ └┘   └──────┘  └─────┘ └──┘ └┘
doc    └──────┘  └──────┘       └──────┘  └─────┘ └──┘
763  begin
st   └─────
764    apply eq_of_bisim (λs1 s2,
id           └─────────┘
src    └────┘└─────────┘  └──────
typ    └────┘└─────────┘  └──────
doc    └────┘             └──────
txt    └────┘             └──────
par    └────┘             └──────
pid                      └──────
st   ─────────────────────────────
765      ∃ s SS, s1 = seq.append s (seq.join (seq.join SS)) ∧
id                                                       
src  ───┘└───┘                                 └─┘
typ  ───┘└───┘                                 └─┘
doc  ───┘ └───┘                                   └─┘ 
txt  ───┘ └───┘                                   └─┘ 
par  ───┘ └───┘                                   └─┘ 
pid  ───┘ └───┘                                   └─┘ 
st   ─────────────────────────────────────────────────────────
766        s2 = seq.append s (seq.join (seq.map join SS))),
id              └────────┘    └──────┘  └─────┘ └──┘
src  ─────┘   └────────┘  └──────┘ └─────┘└──┘  └─┘
typ  ─────┘   └────────┘  └──────┘ └─────┘└──┘  └─┘
doc  ─────┘   └────────┘  └──────┘ └─────┘└──┘  └─┘
txt  ─────┘                                     └─┘
par  ─────┘                                     └─┘
pid  ─────┘                                     └─┘
st   ────────────────────────────────────────────────────┘└─
767    { intros s1 s2 h, exact match s1, s2, h with ._, ._, ⟨s, SS, rfl, rfl⟩ := begin
id                                   └┘  └┘                             └─┘
src      └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘  └┘   └┘└─┘└───┘     
typ      └────────────┘  └────┘     └┘└┘└┘└┘└────┘  └┘  └┘  └┘  └┘   └┘└─┘└───┘     
doc      └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘  └┘   └┘   └───┘     
txt      └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘  └┘   └┘   └───┘     
par      └────────────┘  └────┘       └┘  └┘ └────┘  └┘  └┘  └┘  └┘   └┘   └───┘     
pid            └──────┘              └┘  └┘ └────┘  └┘  └┘  └┘  └┘   └┘   └───┘     
st   ───┘└────────────┘└────────────────────────────────────────────────────────┘└─────
768        apply cases_on s; simp,
id               └──────┘ 
src  ─────┘└────┘└──────┘ └┘└──┘└─
typ  ───────────┘└──────┘└┘└──┘└─
doc  ─────┘└────┘         └┘└──┘└─
txt  ─────┘└────┘         └┘└──┘└─
par  ───────────┘         └┘└──┘└─
pid  ───────────┘         └───────
st   ───────────────────────────┘└─
769        { apply cases_on SS; simp,
id                 └──────┘ └┘
src  ───────┘└────┘└──────┘  └┘└──┘└─
typ  ─────────────┘└──────┘└┘└┘└──┘└─
doc  ───────┘└────┘          └┘└──┘└─
txt  ───────┘└────┘          └┘└──┘└─
par  ─────────────┘          └┘└──┘└─
pid  ─────────────┘          └───────
st   ──────┘└──────────────────────┘└─
770          { intros S SS, cases S with s S; cases s with x s; simp [map],
id                                                                  └─┘
src  ─────────┘└─────────┘└┘└────┘ └───────┘└┘└────┘ └───────┘└┘└────┘└─┘└─
typ  ─────────┘└─────────┘└┘└────┘└───────┘└┘└────┘└───────┘└┘└────┘└─┘└─
doc  ─────────┘└─────────┘└┘└────┘ └───────┘└┘└────┘ └───────┘└┘└────┘└─┘└─
txt  ─────────┘└─────────┘└┘└────┘ └───────┘└┘└────┘ └───────┘└┘└────┘   └─
par  ─────────┘└─────────┘└┘└────┘ └───────┘└┘└────┘ └───────┘└┘└────┘   └─
pid  ────────────────────────────┘ └───────────────┘ └───────────────┘   └──
st   ────────────────────┘└──────────────────────────────────────────────┘└─
771            apply cases_on s; simp,
id                   └──────┘ 
src  ─────────┘└────┘└──────┘ └┘└──┘└─
typ  ───────────────┘└──────┘└┘└──┘└─
doc  ─────────┘└────┘         └┘└──┘└─
txt  ─────────┘└────┘         └┘└──┘└─
par  ───────────────┘         └┘└──┘└─
pid  ───────────────┘         └───────
st   ───────────────────────────────┘└─
772            { exact ⟨_, _, rfl, rfl⟩ },
id                                 └─┘
src  ─────────────────┘ └────┘   └┘└─┘└────
typ  ─────────────────┘ └────┘   └┘└─┘└────
doc  ─────────────────┘ └────┘   └┘   └────
txt  ─────────────────┘ └────┘   └┘   └────
par  ─────────────────┘ └────┘   └┘   └────
pid  ─────────────────┘ └────┘   └┘   └────
st   ──────────┘└──────────────────────┘└─
773            { intros x s,
src  ───────────┘└────────┘└─
typ  ───────────┘└────────┘└─
doc  ───────────┘└────────┘└─
txt  ───────────┘└────────┘└─
par  ───────────┘└────────┘└─
pid  ────────────────────────
st   ─────────────────────┘└─
774              refine ⟨cons x (append s (seq.join S)), SS, _, _⟩; simp } } },
id                       └──┘   └────┘   └──────┘     └┘
src  ───────────┘└─────┘ └──┘  └────┘  └──────┘ └──┘  └─────┘└┘└───┘└──────
typ  ──────────────────┘ └──┘ └────┘ └──────┘└──┘└┘└───────┘└───┘└──────
doc  ───────────┘└─────┘ └──┘  └────┘  └──────┘ └──┘  └─────┘└┘└───┘└──────
txt  ───────────┘└─────┘                        └──┘  └─────┘└┘└───┘└──────
par  ──────────────────┘                        └──┘  └───────┘└───┘└──────
pid  ──────────────────┘                        └──┘  └────────────────────
st   ───────────────────────────────────────────────────────────────────┘└───┘└─
775        { intros x s, exact ⟨s, SS, rfl, rfl⟩ }
id                                └┘       └─┘
src  ───────┘└────────┘└──────┘  └┘  └┘   └┘└─┘└───
typ  ───────┘└────────┘└──────┘ └┘└┘└┘   └┘└─┘└───
doc  ───────┘└────────┘└──────┘  └┘  └┘   └┘   └───
txt  ───────┘└────────┘└──────┘  └┘  └┘   └┘   └───
par  ───────┘└────────┘└──────┘  └┘  └┘   └┘   └───
pid  ─────────────────────────┘  └┘  └┘   └┘   └───
st   ─────────────────┘└────────────────────────┘└─
776      end end },
src  ───────────┘
typ  ───────────┘
doc  ───────────┘
txt  ───────────┘
par  ───────────┘
pid  ──────────┘
st   ──────┘└───┘└┘
777    { refine ⟨nil, SS, _, _⟩; simp }
id               └─┘  └┘
src      └─────┘ └─┘└┘  └─────┘  └───┘
typ      └─────┘ └─┘└┘└┘└─────┘  └───┘
doc      └─────┘ └─┘└┘  └─────┘  └───┘
txt      └─────┘    └┘  └─────┘  └───┘
par      └─────┘    └┘  └─────┘  └───┘
pid                └┘  └─────┘      
st   ────────────────────────────────┘└─
778  end
st   ──┘
779  
780  @[simp] theorem bind_assoc (s : seq1 α) (f : α → seq1 β) (g : β → seq1 γ) :
id                                   └──┘           └──┘           └──┘ 
src                                  └──┘             └──┘             └──┘
typ                                  └──┘           └──┘           └──┘ 
doc    └──┘                          └──┘             └──┘             └──┘
781    bind (bind s f) g = bind s (λ (x : α), bind (f x) g) :=
id     └──┘  └──┘      └──┘             └──┘     
src    └──┘  └──┘         └──┘               └──┘
typ    └──┘  └──┘      └──┘             └──┘     
doc    └──┘  └──┘          └──┘               └──┘
782  begin
st   └─────
783    cases s with a s,
id           
src    └────┘ └───────┘
typ    └────┘└───────┘
doc    └────┘ └───────┘
txt    └────┘ └───────┘
par    └────┘ └───────┘
pid          └───────┘
st   ─────────────────┘└─
784    simp [bind, map],
id           └──┘  └─┘
src    └────┘└──┘└┘└─┘
typ    └────┘└──┘└┘└─┘
doc    └────┘└──┘└┘└─┘
txt    └────┘    └┘   
par    └────┘    └┘   
pid            └┘   
st   ─────────────────┘└─
785    rw [←map_comp],
id          └──────┘
src    └───┘└──────┘
typ    └───┘└──────┘
doc    └───┘        
txt    └───┘        
par    └───┘        
pid      └─┘        
st   ──────────────┘└──
786    change (λ x, join (map g (f x))) with (join ∘ ((map g) ∘ f)),
id                  └──┘  └─┘               └──┘    └─┘     
src    └─────┘  └──┘└──┘ └─┘    └───────┘ └──┘  └─┘ └┘  └┘
typ    └─────┘  └──┘└──┘ └─┘  └───────┘ └──┘  └─┘└┘ └┘
doc    └─────┘  └──┘└──┘ └─┘    └───────┘ └──┘   └─┘ └┘  └┘
txt    └─────┘  └──┘            └───────┘            └┘  └┘
par    └─────┘  └──┘            └───────┘            └┘  └┘
pid            └──┘            └─┘└────┘            └┘  └┘
st   ─────────────────────────────────────────────────────────────┘└─
787    rw [map_comp _ join],
id         └──────┘   └──┘
src    └──┘└──────┘└─┘└──┘
typ    └──┘└──────┘└─┘└──┘
doc    └──┘        └─┘└──┘
txt    └──┘        └─┘    
par    └──┘        └─┘    
pid      └┘        └─┘    
st   ────────────────────┘└──
788    generalize : seq.map (map g ∘ f) s = SS,
id                  └─────┘  └─┘      
src    └───────────┘└─────┘ └─┘   └┘  
typ    └───────────┘└─────┘ └─┘ └┘ 
doc    └───────────┘└─────┘ └─┘   └┘  
txt    └───────────┘              └┘  
par    └───────────┘              └┘  
pid                            └┘  
st   ────────────────────────────────────────┘└─
789    rcases map g (f a) with ⟨⟨a, s⟩, S⟩,
id            └─┘    
src    └─────┘└─┘    └────────────────┘
typ    └─────┘└─┘ └────────────────┘
doc    └─────┘└─┘    └────────────────┘
txt    └─────┘       └────────────────┘
par    └─────┘       └────────────────┘
pid                 └────────────────┘
st   ────────────────────────────────────┘└─
790    apply cases_on s; intros; apply cases_on S; intros; simp,
id           └──────┘                 └──────┘ 
src    └────┘└──────┘   └────┘  └────┘└──────┘   └────┘  └──┘
typ    └────┘└──────┘  └────┘  └────┘└──────┘  └────┘  └──┘
doc    └────┘           └────┘  └────┘           └────┘  └──┘
txt    └────┘           └────┘  └────┘           └────┘  └──┘
par    └────┘           └────┘  └────┘           └────┘  └──┘
pid                                         
st   ─────────────────────────────────────────────────────────┘└─
791    { cases x with x t, apply cases_on t; intros; simp },
id                              └──────┘ 
src      └────┘ └───────┘  └────┘└──────┘   └────┘  └───┘
typ      └────┘└───────┘  └────┘└──────┘  └────┘  └───┘
doc      └────┘ └───────┘  └────┘           └────┘  └───┘
txt      └────┘ └───────┘  └────┘           └────┘  └───┘
par      └────┘ └───────┘  └────┘           └────┘  └───┘
pid            └───────┘                              
st   ───┘└──────────────┘└───────────────────────────────┘└┘
792    { cases x_1 with y t; simp }
id             └─┘
src      └────┘   └───────┘  └───┘
typ      └────┘└─┘└───────┘  └───┘
doc      └────┘   └───────┘  └───┘
txt      └────┘   └───────┘  └───┘
par      └────┘   └───────┘  └───┘
pid              └───────┘      
st   ────────────────────────────┘└─
793  end
st   ──┘
794  
795  instance : monad seq1 :=
id              └───┘ └──┘
src             └───┘ └──┘
typ             └───┘ └──┘
doc                   └──┘
796  { map  := @map,
id              └─┘
src             └─┘
typ             └─┘
doc             └─┘
797    pure := @ret,
id              └─┘
src             └─┘
typ             └─┘
doc             └─┘
798    bind := @bind }
id              └──┘
src             └──┘
typ             └──┘
doc             └──┘
799  
800  instance : is_lawful_monad seq1 :=
id              └─────────────┘ └──┘
src             └─────────────┘ └──┘
typ             └─────────────┘ └──┘
doc                             └──┘
801  { id_map := @map_id,
id               └────┘
src              └────┘
typ              └────┘
802    bind_pure_comp_eq_map := @bind_ret,
id                               └──────┘
src                              └──────┘
typ                              └──────┘
803    pure_bind := @ret_bind,
id                   └──────┘
src                  └──────┘
typ                  └──────┘
804    bind_assoc := @bind_assoc }
id                    └────────┘
src                   └────────┘
typ                   └────────┘
805  
806  end seq1